Dynamic Trace Logic: Definition and Proofs

Technischer Bericht

Autor(en):Bernhard Beckert und Daniel Bruns
Institution:Department of Informatics, Karlsruhe Institute of Technology
Reihe:Karlsruhe Reports in Informatics
Nummer:2012-10
Jahr:2012
URL:https://publikationen.bibliothek.kit.edu/1000028184

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 functional verification of concurrent programs and for proving information-flow properties among other applications.

Anmerkung

A revised version replacing an unsound rule is available at https://formal.kastel.kit.edu/~bruns/papers/trace-tr.pdf.

BibTeX

@TechReport{BeckertBruns12a,
  author	= {Bernhard Beckert and Daniel Bruns},
  title		= {Dynamic Trace Logic: Definition and Proofs},
  year		= 2012,
  month         = oct,
  institution	= {Department of Informatics, Karlsruhe Institute of
		   Technology},
  number	= {2012-10},
  series	= {Karlsruhe Reports in Informatics},
  url		= {https://publikationen.bibliothek.kit.edu/1000028184},
  urn		= {urn:nbn:de:swb:90-281845},
  issn		= {2190-4782},
  license	= {http://creativecommons.org/licenses/by-nc-nd/3.0/},
  language	= {english},
  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 functional
		   verification of concurrent programs and for proving
		   information-flow properties among other applications.},
  note		= {A revised version replacing an unsound rule is available
		   at
		   \url{https://formal.kastel.kit.edu/~bruns/papers/trace-tr.pdf}.}
}