Automatic proofs of properties of simple C-- modules

We address the problem of automatically verifying properties of modules written in the C^-- language, a very simple imperative language. We develop a framework for automatically proving properties of modules written in C^--. Our approach consists of two steps. At the first step, the C^-$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^-- 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 ^-$code alone. We illustrate computer applications on programs computing integers and linked lists