Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Sept. 7, 2005 to Sept. 9, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.1
Thierry Hubert , INRIA Futurs - Universite Paris, France
Claude Marche , INRIA Futurs - Universite Paris, France
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.
C. Marche and T. Hubert, "A case study of C source code verification: the Schorr-Waite algorithm," Third IEEE International Conference on Software Engineering and Formal Methods(SEFM), Koblenz, 2005, pp. 190-199.