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	Reaches	Reachability
⇒•	—	All-path	Universal
⇒◦	—	One-path	Existential
φ, ψ	—	Patterns	Configurations

Metatheory. Sound and relatively complete. Language-independent. Coinductive for loops. Matching logic basis.

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

Limitations. Requires formal semantics. Proof automation challenging. Invariant synthesis. Complexity of semantics.