Loop invariants play a major role in program verification. Though various techniques have been applied to automatic loop invariants generation, most interesting ones often generate only candidate invariants. Thus, a key issue to take advantage of these invariants in a verification process is to check that these candidate loop invariants are actual invariants. This paper introduces a new technique based on constraint programming for automatic verification of inductive loop invariants. This approach is efficient to detect spurious invariants and is also able to verify valid invariants under boundedness restrictions. First experiments on classical benchmarks are very promising.

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.

Abstract The current work of the authors in the area of software tools for automatic construction of compilers is described. This focuses on attempts to provide for automatic production of the semantic‐analysis and intermediate‐code‐generation parts of the Cigale compiler‐writing system, developed at the University of Nice. This work relies on use of the Amsterdam Compiler Kit (ACK) to ensure a full set of optimizers and code generators based on a semi‐universal intermediate language, and, therefore, emphasizes the filling of the gap between parsing and the intermediate language. It is intended as a pragmatic contribution to the automation of the production of true compilers (rather than mere program evaluators) that generate efficient machine code.