一句话：提出语言无关的全路径可达性逻辑，以操作语义为公理证明非确定性程序的部分正确性。
本文研究如何为用非确定性（如并发）语言编写的程序，证明其全路径可达性属性。作者提出全路径可达性逻辑：它把任意无条件操作语义作为公理，推导“满足前置条件的状态在所有终止执行路径上都到达满足后置条件的状态”这一部分正确性性质。该证明系统独立于对象语言，并具有可靠性与相对完备性。论文给出了该逻辑的证明系统及元理论结果；其可靠性已在 Coq 中机器化验证，该方法还作为 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 in Coq. This approach is implemented in a tool for semantics-based verification as part of the K framework (http://kframework.org)
@article{paperbot799,
title = {All-Path Reachability Logic},
author = {Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:5)2019}
}