Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)

Koblenz, Germany

Sept. 7, 2005 to Sept. 9, 2005

ISBN: 0-7695-2435-4

pp: 190-199

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.1

Claude Marche , INRIA Futurs - Universite Paris, France

Thierry Hubert , INRIA Futurs - Universite Paris, France

ABSTRACT

We describe an experiment of formal verification of C source code, using the CADUCEUS tool.We performed a full formal proof of the classical Schorr-Waite graph-marking algorithm, which has already been used several times as a case study for formal reasoning on pointer programs. Our study is original with respect to previous experiments for several reasons. First, we use a general-purpose tool for C programs: we start from a real source code written in C, specified using an annotation language for arbitrary C programs. Second, we use several theorem provers as backends, both automatic and interactive. Third, we indeed formally establish more properties of the algorithm than previous works, in particular a formal proof of termination is made^1.

INDEX TERMS

null

CITATION

Claude Marche,
Thierry Hubert,
"A case study of C source code verification: the Schorr-Waite algorithm",

*Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)*, vol. 00, no. , pp. 190-199, 2005, doi:10.1109/SEFM.2005.1