Exploring Different Constraint-Based Modelings for Program Verification

Recently, constraint-programming techniques have been used to generate test data and to verify the conformity of a program with its specification. Constraint generated for these tasks may involve integer ranging on all machine-integers, thus, the constraint-based modeling of the program 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 ive. We outline the key role of Boolean abstractions and explore different search strategies on standard benchmarks.

• Type: Conference
• Year: 2007
• Where: CP
• Authors: Hélène Collavizza, Michel Rueher
• Keywords: Artificial Intelligence, Constraint-based Modeling, Constraint-programming Techniques, CP 2007, Test Data