@techreport{rosu-stefanescu-ciobaca-moore-2012-tr,
author = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu and \c{S}tefan
Ciob\^{a}c\u{a} and Brandon M. Moore},
title = {Reachability Logic},
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.
},
institution = {University of Illinois},
month = {Jul},
year = {2012},
number = {http://hdl.handle.net/2142/32952},
author_id = {Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and
Brandon Moore},
category = {fsl, executable_semantics, logics, matching_logic,
program_verification, programming_languages},
project_url = {http://fsl.cs.uiuc.edu/rl},
project_name = {Reachability Logic},
hidden = {false},
}