up: Publications |
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 |
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 = {https://www.irit.fr/~Martin.Strecker/Publications/lopstr10.html}, year = 2011 }
Last modified: Fri Aug 26 13:32:58 CEST 2011 |