CeV Constraints and Verification ...
CeV (Constraint and Verification) gathers know-how from constraint programming and program verification. CeV investigates the use of constraint programming technics for program verification, one of the most critical issue in software engineering. Recently, constraint programming has been successfully applied to different verification fields, ranging from automatic test case generation to the automatic detection of non-conformances between a program and its specification. Within this framework, Cev mainly addresses the following issues:
  • Automatic detection of non-conformances between a program and its specification: When a program is bounded, either thanks to is own structure or to user given bounds, constraint programming can be used to detect non-conformances between the program and its specification. The program is first translated to a relational form using dynamic or static single assignments and combined with a negation of its specification. A solver is then be used to find some solution to this constraint problem, each of them being a counter example that show a non conformance between the program and its specification. The main challenge is to build an efficient solving process adapted to the verification problem.
  • Combining abstract interpretation and constraint programming: Abstract interpretation and constraint programming are technics that have the capability to determine domain values of program variables. While the first has shown some abilities to handle big piece of software, the latter scale up scarcely. And, while contraint programming often allows to compute domain values quite precisely, sometimes abstract interpretation computes them with too large approximations and thus, produces some false alarms. CeV attempts to combine the strength of these two technics to get a tool that scale up and computes tight domain values.
  • Helping error localization: Using constraint programming to automatically detect non-conformances of a program with its specification produces counter examples that should help the user to understand program failures. However, such a counter example does not actually localize the error. Constraint programming could be used to help the user to localize the error by computing the subsets of the program that do not contradict the counter example and the specification. The issue here is to compute the most relevant subsets and to provide useful informations.
  • Floating point constraints: Verifying programs that use floating point computations requires dedicated constraints with the capability to handle floating point arithmetic peculiarities. The latter can not be correctly handled by means of solvers over the real numbers that looses some solutions over the floating point numbers. Therefore, developping dedicated solvers is required to provide a correct analysis of programs with floating point computations.
Cev is a member of the MDSC team from I3S, a joint research centre of university of Nice and CNRS.