Reachability Logic

Origin. Roșu et al. (2012). Language-independent program verification. Reachability rules: φ ⇒ ψ. Derived from operational semantics. Foundation for K framework verification.

Models. Configurations: program states with structure. Reachability claims: one pattern reaches another. Sound and complete relative to operational semantics. Language-parametric.

Formalism.

Configurations: Terms in a configuration sort. Encode: code, environment, heap, etc. Example: ⟨code, env, heap⟩

Patterns: First-order formulas over configurations. φ: configurations matching φ.

Reachability claim: φ ⇒ ψ "Any configuration matching φ reaches one matching ψ"

All-path vs one-path: φ ⇒• ψ: all paths reach ψ φ ⇒◦ ψ: one path reaches ψ (existential)

Proof system: Axiom: operational semantics step Transitivity: φ ⇒ ψ, ψ ⇒ χ / φ ⇒ χ Case analysis: φ ⇒ ψ₁, φ ⇒ ψ₂ / φ ⇒ ψ₁ ∨ ψ₂ Circularity: co-inductive reasoning

Circularity rule: C ∪ {φ ⇒ ψ} ⊢ φ ⇒ • ∨ ψ' ψ' ⊢ ψ ────────────────────────────────────── C ⊢ φ ⇒ ψ where • is intermediate progress.

Example: ⟨while(b){s}, σ⟩ ∧ b(σ) ⇒ ⟨while(b){s}, σ'⟩ ∧ INV(σ')

Matching logic foundation: Reachability claims as matching logic formulas. Unified framework.

Symbols.

Symbol	Unicode	Name	Meaning
⇒	U+21D2	Rightwards double arrow / Reachability	φ ⇒ ψ : a φ-configuration reaches a ψ-configuration
⇒•	—	All-path reachability	Every path reaches the target
⇒◦	—	One-path reachability	Some path reaches the target
•	U+2022	Bullet / Progress	At least one semantic step has been taken
◦	U+25E6	White bullet / Existential marker	Marks the one-path variant
φ, ψ, χ	—	Patterns	Matching-logic formulas over configurations
⟨	U+27E8	Mathematical left angle bracket	Opens a configuration term
⟩	U+27E9	Mathematical right angle bracket	Closes a configuration term
∧	U+2227	Conjunction	Constrains a pattern by a side condition
∨	U+2228	Disjunction	Case analysis on successor configurations
∪	U+222A	Union	Adds a circular claim to the hypothesis set C
⊢	U+22A2	Turnstile / Derivability	C ⊢ φ ⇒ ψ, derivable from hypotheses C
σ	U+03C3	Sigma / Store	Valuation component of a configuration
C	—	Circularity set	Claims usable as hypotheses after progress
INV	—	Invariant pattern	The circular claim supplied for a loop

Metatheory. The result that gives the system its point is language-independence with soundness and relative completeness: a fixed, small proof system, parameterized only by the target language's operational semantics presented as a set of reachability rules, derives every valid reachability property of that language, relative to an oracle for the matching-logic theory of configurations. Roșu and Ștefănescu established this for one-path reachability (2012–2013) and then for all-path reachability, which is the version needed for nondeterministic and concurrent languages. The consequence is that Hoare logic ceases to be a primitive: the axiomatic semantics of IMP is derivable from IMP's operational semantics inside the reachability proof system, so a per-language program logic no longer has to be designed and separately proved sound. Circularity is the rule that replaces the invariant rule, and it is coinductive — a claim may be assumed as a hypothesis only after the derivation has taken at least one semantic step, and this progress condition is exactly what keeps the coinduction well-founded rather than circular. Patterns are matching-logic formulas, simultaneously terms and predicates, so a single formalism carries both the configuration structure and the assertions about it.

Applies to. K framework. Language-independent verification. Compiler verification. Smart contracts. Runtime verification.

Limitations. Completeness is relative in Cook's sense: the proof system reduces reachability to implications between patterns, and those are discharged by an oracle for matching logic, whose validity problem is undecidable — matching logic subsumes first-order logic with least fixed points. The circularity rule supplies no invariant; it only licenses using a claim once progress has been made, so the loop assertion is still an input, and the progress side condition means claims that must be discharged without taking a step cannot be closed. What the judgements express is reachability of a target pattern, so temporal properties in general — fairness, recurrence, "infinitely often" — are not reachability claims and cannot be stated. The entire enterprise is parameterized by a complete formal operational semantics of the target language, and every proof is sound only relative to that semantics: an inaccuracy in modelling the language transfers silently into every verification built on it.