Automatic Proofs of Properties of Simple C- Modules

Abstract

We address the problem of automatically verifying properties of modules written in the C/sup --/ language, a very simple imperative language. We develop a framework for automatically proving properties of modules written in C/sup --/. Our approach consists of two steps. At the first step, the C/sup -$/module is automatically transformed into a set of axioms written in the language of equational logic. This transformation is bused on the algebraic semantics of C/sup --/ modules. At the second step, the theorem prover NICE is used to mechanically perform the proof of the desired properties. Our system enables us to prove many properties completely automatically from the C/sup -$/code alone. We illustrate computer applications on programs computing integers and linked lists.