Home  |  english  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Dynamic Logic with Trace Semantics

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert und Daniel Bruns
In:24th International Conference on Automated Deduction (CADE-24)
Verleger:Springer-Verlag
Reihe:Lecture Notes in Computer Science
Band:7898
Jahr:2013
Seiten:315-329
URL:http://link.springer.com/chapter/10.1007/978-3-642-38574-2_22
DOI:10.1007/978-3-642-38574-2_22

Abstract

Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic (DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for proving functional and information-flow properties in concurrent programs, among other applications.

BibTeX

@InProceedings{BeckertBruns2013,
  author	= {Bernhard Beckert and Daniel Bruns},
  title		= {Dynamic Logic with Trace Semantics},
  booktitle	= {24th International Conference on Automated Deduction
		   (CADE-24)},
  editor	= {Maria Paola Bonacina},
  year		= 2013,
  month		= jun,
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= 7898,
  pages		= {315--329},
  isbn		= {978-3-642-38573-5},
  language	= {english},
  doi		= {10.1007/978-3-642-38574-2_22},
  url		= {http://link.springer.com/chapter/10.1007/978-3-642-38574-2_22},
  abstract	= {Dynamic logic is an established instrument for program
		   verification and for reasoning about the semantics of
		   programs and programming languages. In this paper, we
		   define an extension of dynamic logic, called Dynamic Trace
		   Logic (DTL), which combines the expressiveness of program
		   logics such as dynamic logic with that of temporal logic.
		   And we present a sound and relatively complete sequent
		   calculus for proving validity of DTL formulae. Due to its
		   expressiveness, DTL can serve as a basis for proving
		   functional and information-flow properties in concurrent
		   programs, among other applications.}
}