A case study of C source code verification: the SchorrWaite algorithm

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. Keywords: Formal verification, Floyd-Hoare logic, Pointer programs, Aliasing, C programming language. The Schorr-Waite algorithm is the first moutain that any formalism for pointer aliasing should climb. — Richard Bornat ([4], page 121) 1