N. Bertot and . Magaud, pour toutes nos discussions sur les spécifications et preuves en Coq, et les rapporteurs

]. Bibliographie1 and . Abrial, Event Based Sequential Program Development: Application to Constructing a Pointer Program, 13th Symp. FME'2003, pp.51-74, 2003.

Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

R. Bornat, Proving Pointer Programs in Hoare Logic, 5th Conf. on Mathematics of Program Construction, MPC'00, pp.102-126, 2000.
DOI : 10.1007/10722010_8

J. Dufourd, Schorr-Waite Coq Development In-line Documentation, 2011.

J. Dufourd, Verifying Linked Representations of Linear Algebraic Data Types in Coq, 2011.

J. Dufourd and Y. Bertot, Formal Study of Plane Delaunay Triangulation, Interactive Theorem Proving, ITP'2010, pp.211-226, 2010.
DOI : 10.1007/978-3-642-14052-5_16
URL : https://hal.archives-ouvertes.fr/inria-00504027

M. Giorgino, Verification of the Schorr-Waite Algorithm ??? From Trees to Graphs, 20th Logic Based Prog. Synth. and Transf., LOPSTR'2010, pp.67-83, 2010.
DOI : 10.1145/363534.363554
URL : https://hal.archives-ouvertes.fr/hal-00601440

G. Gonthier, Formal Proof -The Four-Color Theorem. Notices of the, pp.1382-1393, 2008.

D. Gries, The Schorr-Waite graph marking algorithm, Acta Informatica, vol.4, issue.3, pp.223-232, 1979.
DOI : 10.1007/BF00289068

T. Hubert and C. Marché, A case study of C source code verification: the Schorr-Waite algorithm, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp.190-199, 2005.
DOI : 10.1109/SEFM.2005.1

X. Leroy and S. Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, pp.1-31, 2008.
DOI : 10.1007/s10817-008-9099-0
URL : https://hal.archives-ouvertes.fr/inria-00289542

A. Loginov, T. Reps, and M. Sagiv, Automatic Verification of the Deutsch-Schorr-Waite Tree Traversal Algorithm, 13th SAS, pp.261-274, 2006.

F. Mehta and T. Nipkow, Proving pointer programs in higher-order logic, Information and Computation, vol.199, issue.1-2, pp.200-227, 2005.
DOI : 10.1016/j.ic.2004.10.007

H. Schorr and W. R. Waite, An efficient machine-independent procedure for garbage collection in various list structures, Communications of the ACM, vol.10, issue.8, pp.501-506, 1967.
DOI : 10.1145/363534.363554

R. E. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010

M. Ward, Derivation of data intensive algorithms by formal transformation: the Schnorr-Waite graph marking algorithm, IEEE Transactions on Software Engineering, vol.22, issue.9, pp.665-686, 1996.
DOI : 10.1109/32.541437