All-Path Reachability Logic

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.

Sidebar