[isabelle] New AFP entries: Data Refinement and Graph Marking

Semantics and Data Refinement of Invariant Based Programs
Viorel Preoteasa and Ralph-Johan Back

The invariant based programming is a technique of constructing correct
programs by first identifying the basic situations (pre- and
post-conditions and invariants) that can occur during the execution of
the program, and then defining the transitions and proving that they
preserve the invariants. Data refinement is a technique of building
correct programs working on concrete datatypes as refinements of more
abstract programs. In the theories presented here we formalize the
predicate transformer semantics for invariant based programs and their
data refinement.

Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using
Data Refinement
Viorel Preoteasa and Ralph-Johan Back

The verification of the Deutsch-Schorr-Waite graph marking algorithm is
used as a benchmark in many formalizations of pointer programs. The main
purpose of this mechanization is to show how data refinement of
invariant based programs can be used in verifying practical algorithms.
The verification starts with an abstract algorithm working on a graph
given by a relation {\em next} on nodes. Gradually the abstract program
is refined into Deutsch-Schorr-Waite graph marking algorithm where only
one bit per graph node of additional memory is used for marking.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.