### Pointer Program Derivation using Coq: Graphs and Schorr-Waite Algorithm

We present a specification, a derivation and total correctness proofs of operations for bi-functional graphs implemented with pointers, including the Schorr-Waite algorithm. This one marks such a graph with an economical depth-first strategy. Our approach is purely algebraic and functional, from a simple graph specification to the simulation of a tail-recursive imperative program, then to a true C pointer program by elementary classical transformations. We stay in the unique higher-order formalism of the Calculus of Inductive Constructions for specifications, programs and proofs. All the development is supported by Coq.

J-F. Dufourd

ICFEM , Volume 8829 , page 139-154 - 2014

International conference with proceedings Pointer Program Derivation using Coq: Graphs and Schorr-Waite Algorithm, ICFEM, Luxembourg, Luxembourg, pages 139-154, Springer-Verlag, LNCS, Volume 8829, novembre 2014, doi:10.1007/978-3-319-11737-9_10 Research team : IGG

@Inproceedings{4-Dufo14a,
author = {Dufourd, J-F.},
title = {Pointer Program Derivation using Coq: Graphs and Schorr-Waite Algorithm},
booktitle  = {ICFEM},
series = {LNCS},
volume = {8829},
pages = {139-154},
month = {Nov},
year = {2014},
publisher = {Springer-Verlag},
doi = {10.1007/978-3-319-11737-9_10},
x-international-audience = {Yes},
x-language = {EN},
url = {http://icube-publis.unistra.fr/4-Dufo14a}
}


See publications of the same authors