Dynamic Logic with Trace Semantics

Dynamic Logic with Trace Semantics
复制标题

具有跟踪语义的动态逻辑

DOI：
10.1007/978-3-642-38574-2_22
复制
发表时间：
2013
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
通讯作者：
Daniel Grahl
Daniel Grahl
中科院分区：
--
文献类型：
--
作者：
Bernhard Beckert;Daniel Grahl

文献摘要

被引文献

相似文献

动态逻辑是程序验证和对程序和编程语言的语义进行推理的既定工具。本文定义了动态逻辑的一种扩展，即动态跟踪逻辑（dynamic Trace logic， DTL），它将动态逻辑等程序逻辑的表达性与时间逻辑的表达性相结合。并给出了一个较完善的序贯演算来证明DTL公式的有效性。
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.