All-Path Reachability Logic
Andrei Stefanescu and Brandon Moore and Stefan Ciobaca and Radu Mereuta and Traian Serbanuta and Grigore Rosu
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 K framework.
Project(s): K
Grant(s): DAK