M.: Exploring different constraint-based modelings for program verification

Abstract. Recently, constraint-programming techniques have been used togenerate test dataand toverify the conformity of aprogramwith its spec-ification. Constraint generated for these tasks may involve integer ranging on all machine-integers, thus, the constraint-based modeling of the pro-gram and its specification is a critical issue. In this paper we investigate different models. We show that a straightforward translation of a program and its specification in a system of guarded constraints is ineffective. We outline the key role of Boolean abstractions and explore different search strategies on standard benchmarks.