All-Path Reachability Logic
All-Path Reachability Logic
复制标题
全路径可达性逻辑
DOI：
10.23638/lmcs-15(2:5)2019
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Grigore Roşu
中科院分区：
文献类型：
--
作者：
Andrei Stefanescu;Ștefan Ciobâcă;Radu Mereuta;Brandon M. Moore;Traian;Grigore Roşu
本文提出了一个独立于语言的证明系统的可达性的非确定性（如并发）的语言编写的程序，称为全路径可达性逻辑。它通过全路径语义（满足给定前提条件的状态到达满足所有终止执行路径上的给定后置条件的状态）导出部分正确性属性。证明系统以任何无条件的操作语义为公理，并且是可靠的（部分正确的）和（相对）完整的，独立于对象语言;可靠性也被机械化了（Coq）。这种方法在作为\（\mathbb K\）框架一部分的基于语义的验证工具中实现。
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g. concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized (Coq). This approach is implemented in a tool for semantics-based verification as part of the \(\mathbb K\) framework.