Reachability Logic

Rosu, Grigore; Stefanescu, Andrei; Ciobaca, Stefan; Moore, Brandon

Permalink

https://hdl.handle.net/2142/32952 Copy

Description

Title

Reachability Logic

Author(s)

• Rosu, Grigore
• Stefanescu, Andrei
• Ciobaca, Stefan
• Moore, Brandon

Issue Date

2012-07

Keyword(s)

• Reachability logic
• Matching logic
• Operational semantics
• Program verification

Abstract

Abstract. This paper introduces *reachability logic*, a language-independent seven-rule proof system for deriving reachability properties of systems. The key ingredients of *reachability logic* are its sentences, which are called reachability rules and generalize the transitions of operational semantics and the Hoare triples of axiomatic semantics, and the *Circularity* proof rule, which generalizes invariant proof rules for iterative and recursive constructs in axiomatic semantics. The target transition system is described as a set of reachability rules, which are taken as axioms in a reachability logic proof. Typical definition styles which can be read as collections of reachability rules include conventional small-step and big-step operational semantics. The reachability logic proof system is shown sound (in the sense of partial correctness) and relatively complete. The soundness result has also been formalized in Coq, allowing to convert reachability logic proofs into proof certificates depending only on the operational semantics and the unavoidable domain reasoning. 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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/32952

Owning Collections