Email Gateway (Aug 18 2022 at 15:23): Email Gateway (Aug 18 2022 at 15:23):From: Tobias Nipkow <nipkow@in.tum.de>
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.
http://afp.sourceforge.net/entries/DataRefinementIBP.shtml
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.
http://afp.sourceforge.net/entries/GraphMarkingIBP.shtml
Last updated: Apr 26 2024 at 12:28 UTC