All-Path Reachability Logic

ABSTRACT. This paper presents a language-independent proof system for proving reachability properties of programs written in non-deterministic (concurrent) languages. The proof system can derive properties with either all-path and one-path semantics, that is, that states satisfying a given precondition reach states satisfying a given postcondition on all terminating execution paths, respectively on one terminating execution path. The proof system may be instantiated with any unconditional operational semantics, and is shown sound (i.e., partially correct) and (relatively) complete, independent of the object language. The proof system is implemented in a tool for semantics-based verification as part of the K framework, and evaluated on a few examples.