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

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

Conference version: PDF

Extended version: PDF

BibTeX Entry

@incollection {GiSt2010SchorrWaite,
   author = {Giorgino, Mathieu and Strecker, Martin and Matthes, Ralph and Pantel, Marc},
   affiliation = {IRIT (Institut de Recherche en Informatique de Toulouse), Universit{\'e} de Toulouse, France},
   title = {Verification of the Schorr-Waite Algorithm – From Trees to Graphs},
   booktitle = {Logic-Based Program Synthesis and Transformation},
   series = {Lecture Notes in Computer Science},
   editor = {Alpuente, María},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-20550-7},
   keyword = {Computer Science},
   pages = {67-83},
   volume = 6564,
   doi = {http://dx.doi.org/10.1007/978-3-642-20551-4_5},
   url = {http://www.irit.fr/~Martin.Strecker/Publications/lopstr10.html},
   year = 2011
}