# One-Path Reachability Logic

This paper introduces (one-path) reachability logic, a

language-independent proof system for program verification, which

takes an operational semantics as axioms and derives reachability

rules, which generalize Hoare triples. This system improves on

previous work by allowing operational semantics given with conditional

rewrite rules, which are known to support all major styles of

operational semantics. In particular, Kahn’s big-step and Plotkin’s

small-step semantic styles are now supported. The reachability logic

proof system is shown sound (i.e., partially correct) and (relatively)

complete. Reachability logic thus eliminates the need to independently

define an axiomatic and an operational semantics for each language,

and the non-negligible effort to prove the former sound and complete

w.r.t. the latter. The soundness result has also been formalized in

Coq, allowing reachability logic derivations to serve as formal proof

certificates that rely only on the operational semantics.