Dynamic Logic with Trace Semantics
Bernhard Beckert and Daniel Bruns
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.