Euclide is a new Constraint-Based Testing tool for verifying safety-critical C programs. By using a mixture of symbolic and numerical analyses (namely static single assignment form, constraint propagation, integer linear relaxation and search-based test data generation), it addresses three distinct applications in a single framework: structural test data generation, counter-example generation and partial program proving.
The core algorithm of the tool takes as input a C program and a point to reach somewhere in the code. As a result, it outcomes either a test datum that reaches the selected point, or an ``unreachable'' indication showing that the selected point is unreachable. Optionally, the tool takes as input additional safety properties that can be given under the form of pre/post conditions in ACSL or assertions directly written in the code. In this case, Euclide can either prove that these properties or assertions are verified or find a counter-example when there is one. As these problems are undecidable in the general case, Euclide only provides a semi-correct procedure (when it terminates, it provides the right answer) for them.
The underlying technology of the tool is Constraint Programming. It implements several dedicated constraint solvers based on constraint propagation, linear relaxations and labeling.
Current Research works around the tool focus on modular integers and floating-point computations and better constraint solving procedures based on relational abstract domains computations.
Euclide has been registered with the APP under reference IDDN.FR.001.250011.000.S.P.2009.000.10600.