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.

Proofs by induction arc important in many computer science and artificial intelligence applications, in particular, in program verification and specification systems. We present a new method to prove (and disprove) automatically inductive properties. Given a set of axioms, a well-suited induction scheme is constructed automatically. We call such an induction scheme a test set. Then, for proving a property, we just instantiate it with terms from the test set and apply pure algebraic simplification to the result. This method needs no completion and explicit induction. However it retains their positive features, namely, the completeness of the former and the robustness of the latter. It has been implemented in the theorem-prover SPIKE.