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.

@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.}
}