Verification of the Schorr-Waite Algorithm - From Trees to Graphs

Mathieu Giorgino (1) , Martin Strecker (2) , Ralph Matthes (2, 3) , Marc Pantel (2, 4)

1 IRIT - Institut de recherche en informatique de Toulouse
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 CNRS - Centre National de la Recherche Scientifique
4 Toulouse INP - Institut National Polytechnique (Toulouse)

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 re finement of a functional one working on trees. It is composed of two orthogonal steps of re finement -- functional to imperative and tree to graph -- fi nally merged to obtain the result. Our imperative speci fications use monadic constructs and syntax sugar, making them close to common imperative languages. This work has been realized within the Isabelle/HOL proof assistant.

Mots clés: program refinement; Verification of imperative programs; Pointer algorithms

Domaines: Théorie et langage formel [cs.FL]; Algorithme et structure de données [cs.DS]; Génie logiciel [cs.SE]

Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel. Verification of the Schorr-Waite Algorithm - From Trees to Graphs. Logic-Based Program Synthesis and Transformation, Jul 2010, Hagenberg, Austria. pp.67-83, ⟨10.1007/978-3-642-20551-4_5⟩. ⟨hal-00601440⟩