Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement

Viorel Preoteasa 🌐 and Ralph-Johan Back 🌐

May 28, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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

License

BSD License

History

January 5, 2012
Updated for the new definition of data refinement and the new syntax for demonic and angelic update statements

Topics

Session GraphMarkingIBP

Depends on

Cite

× 
@article{GraphMarkingIBP-AFP,
  author  = {Viorel Preoteasa and Ralph-Johan Back},
  title   = {Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2010},
  note    = {\url{https://isa-afp.org/entries/GraphMarkingIBP.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: