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

- Computer science/Algorithms/Graph

### Session GraphMarkingIBP

- Graph
- SetMark
- StackMark
- LinkMark
- DSWMark

### Depends on

- Semantics and Data Refinement of Invariant Based Programs

## Cite

×

GraphMarkingIBP-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Mar 15, 2012 : Isabelle2011-1
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- May 28, 2010 : Isabelle2009-1