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