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
Additionnal material

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