Verification of the Schorr-Waite algorithm - From trees to graphs

Mathieu Giorgino, Martin Strecker, Ralph Matthes and Marc Pantel


Abstract

This article proposes a method for proving the correctness of graph algorithms by manipulating their spanning trees enriched with additional references. We illustrate this concept with a proof of the correctness of a (pseudo-)imperative version of the Schorr-Waite algorithm by refinement of a functional one working on trees. It is composed of two orthogonal steps of refinement - functional to imperative and tree to graph - finally merged to obtain the result.

Our imperative specifications use monadic constructs and syntax sugar, making them close to common imperative languages. This work has been realized within the Isabelle/HOL proof assistant.

Online Copy

PDF

Extended version: PDF

Files

Isabelle 2009-2 theories: SW_isabelle2009-2.tar.gz

Bibtex Entry

(preliminary) 

@INPROCEEDINGS{GiSt2010SchorrWaite,
  author = {Giorgino, Mathieu and Strecker, Martin and Matthes, Ralph and Pantel, Marc},
  title = {{Verification of the Schorr-Waite algorithm – From trees to graphs}},
  booktitle = {{Logic-Based Program Synthesis and Transformation (LOPSTR)}},
  year = {2010},
  institution = {{IRIT (Institut de recherche en Informatique de Toulouse)}},
  keywords = {Isabelle, Verification of imperative programs, Pointer algorithms, Program refinement},
  language = {english},
  url = {http://www.irit.fr/~Mathieu.Giorgino/Publications/GiSt2010SchorrWaite.html}
}