Paper Info
Title
Dynamic logic with trace semantics
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.
Year
DOI
Venue
2013
10.1007/978-3-642-38574-2_22
CADE
Keywords
Field
DocType
dynamic logic,concurrent program,temporal logic,established instrument,dtl formula,trace semantics,sequent calculus,information-flow property,programming language,dynamic trace logic,program verification
Discrete mathematics,Computational logic,Temporal logic of actions,Programming language,Computer science,Multimodal logic,Description logic,Substructural logic,Algorithm,Dynamic logic (digital electronics),Higher-order logic,Dynamic logic (modal logic)
Conference
Citations 
PageRank 
References 
2
0.40
9
Authors
2
Name
Order
Citations
PageRank
Bernhard Beckert186286.50
Daniel Bruns2764.96