Reachability Logic in K

Abstract. This paper presents a language-independent proof system for reacha-bility properties of programs written in non-deterministic (concurrent) languages, referred to as reachability logic. The proof system derives partial-correctness properties with either all-path or one-path semantics, i.e., that states satisfying a given precondition reach states satisfying a given postcondition on all execu-tion paths, respectively on one execution path. Reachability logic takes as axioms any unconditional operational semantics, and is sound (i.e., partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized. The proof system is implemented in a tool for semantics-based verification as part of the K framework, and evaluated on a few examples.