# Difference between revisions of "Reachability Logic - Supporting Material"

(→Coq Proofs) |
(Describe inidvidual files in All-Path section) |
||

Line 25: | Line 25: | ||

* [http://code.google.com/p/matching-logic/source/browse/trunk?r=564#trunk%2Fcoq%2Fmixed_shallow coq/mixed_shallow] | * [http://code.google.com/p/matching-logic/source/browse/trunk?r=564#trunk%2Fcoq%2Fmixed_shallow coq/mixed_shallow] | ||

+ | |||

+ | Description of files: | ||

+ | |||

+ | * [http://code.google.com/p/matching-logic/source/browse/trunk/coq/mixed_shallow/proofsystem.v?r=564 proofsystem.v] the syntax of the proof system | ||

+ | * [http://code.google.com/p/matching-logic/source/browse/trunk/coq/mixed_shallow/reduction.v?r=564 reduction.v] some basic definitions about paths and termination in the transitive closure of a relation. | ||

+ | * [http://code.google.com/p/matching-logic/source/browse/trunk/coq/mixed_shallow/generic_soundness.v?r=564 generic_soundness.v] a generic soundness proof, parameterized over the semantics (all-path or one-path) to assign rules and reducing soundness to the proof system to a few lemmas about the chosen semantics. | ||

+ | * [http://code.google.com/p/matching-logic/source/browse/trunk/coq/mixed_shallow/generic_ex.v?r=564 generic_ex.v] instantiating the generic proof to soundness of one-path (EXists-path) conclusions. | ||

+ | * [http://code.google.com/p/matching-logic/source/browse/trunk/coq/mixed_shallow/generic_all.v?r=564 generic_all.v] instantiating the generic proof to soundness of all-path conclusions. | ||

===One-Path Reachability with Conditional Rules=== | ===One-Path Reachability with Conditional Rules=== |

## Latest revision as of 16:41, 16 October 2013

This page organizes proofs, tools, and example code related to reachability logic.

## Contents |

## [edit] Technical Report

**Reachability Logic**- Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
http://hdl.handle.net/2142/32952, July 2012**Technical Report**

*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.

## [edit] Examples

Here are Maude files demonstrating how various styles of operational semantics can all be faithfully expressed with rewriting rules:

The files imp-bigstep/imp-bigstep.maude and imp-smallstep/imp-smallstep.maude show how small-step and big-step semantics can be encoded. Running the test.maude file from either directory like "maude imp-bigstep/test.maude" will execute some test programs under the corresponding semantics.

## [edit] Tools

MatchC is a verifier for an idealized fragment of C. The proof strategy is based on set circularity, taking annotations of initial invariants as the set of circularities and using symbolic execution to attempt to complete the proofs.

## [edit] Coq Proofs

### [edit] All-Path and One-Path Reachability Logic

The newest development in reachability logic is a proof system which can derive all-path rules, saying that in a nondeterministic language every execution path reaches the target pattern. The proof system covers all-path and one-path properties, and we give a soundness proof covering both in this directory:

Description of files:

- proofsystem.v the syntax of the proof system
- reduction.v some basic definitions about paths and termination in the transitive closure of a relation.
- generic_soundness.v a generic soundness proof, parameterized over the semantics (all-path or one-path) to assign rules and reducing soundness to the proof system to a few lemmas about the chosen semantics.
- generic_ex.v instantiating the generic proof to soundness of one-path (EXists-path) conclusions.
- generic_all.v instantiating the generic proof to soundness of all-path conclusions.

### [edit] One-Path Reachability with Conditional Rules

Another current version of reachability logic of incomparable power derives only one-path reachability rules, but supports reasoning about languages defined with conditional rules.

The following files define the minimal assumptions on a configuration space and pattern and formula languages to instantiate matching logic, gives the rules of the proof system, and proves it is sound:

- Terms.v The term language
- Model.v Configuration model
- AbstractML.v Abstract Matching Logic
- Closure.v Transitive/reflexive closure helpers
- Patterns.v Matching logic patterns
- Satisfaction.v Satisfaction relation of patterns
- Reachability.v Reachability Rules
- ProofSystem.v The proof system
- Soundness.v The soundness theorem

An older soundness proof with slightly different notation for the conditional system can be found here:

This proves some derived rules:

### [edit] Proofs for the system without conditional rules

Much more has been proved about unconditional reachability systems.

The description and soundness of the proof system is split into four files:

- matchingl.v Defines the properties needed of a domain, pattern language, formula language, and satisfaction relation to apply matching logic.
- matchinglproofsystem.v Defines the proof system
- matchinglreduction.v Various definitions relating reachability rules and transitions systems, including semantic soundness of a reachability rule and how to generate a transition system from a set of rules.
- matchinglpartialcorrectness.v Proves soundness of the proof system.

For applications that do not require an exotic syntax of formulas or patterns, generic.v constructs acceptable definitions of patterns, formulas, and satisfaction for any given Sigma-algebra. Uses a locally nameless representation for quantifiers. This also demonstrates that the assumptions in matchingl.v are consistent.

The language IMP was defined in a few semantic styles, taking idiomatic Coq definitions of program configurations as the domain of the matching logic, and also showing that a direct definition of a transition system was equivalent to the transition system induced by reachability rules.

- domains.v Defines program configurations for evaluation contexts and k-style definitions, including contexts.
- model.v Defines sorts and function symbols needed for a Sigma-algebra over the domains. This includes all the operations and domains, each particular language definition uses just a subset.

Here are the language definitions

- contexts.v Evaluation-contexts style semantics, both directly defined as a transition relation and presented as reachability rules, with a proof of equivalence.
- BigStep.v Direct definition of a transition relation for a big-step semantics. No reachability rules as this was written before the proof system was extended to conditional rules.
- smallstep.v Direct definition of a transition relation for a small-step semantics.
- kstyle.v Direct definition and reachability rules defining a K-style semantics for imp. Reachability rules are based on the Maude program generated from the example K definition imp.k.

For the two styles which could be defined with unconditional rules, a proof was made about a simple program.

- impproofs.v Proves a statement about the sum program with the evaluation-contexts semantics. This requires a lot of domain reasoning about the context-decomposition and plugging operations, which is partially automated but still makes the proof slow to check.
- kproofs.v Proves an equivalent statement in the k-style semantics.