University of Illinois Urbana-Champaign

Reachability Logic

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

Content Files
rosu-stefanescu-ciobaca-moore-2012-tr.pdf

Permalink

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

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
Date of Ingest
2012-07-18T19:39:05Z
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
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/32952

Owning Collections

Research and Tech Reports - Computer Science PRIMARY