The SOPRANO project is a research project funded by the ANR (French National Research Agency) whose aim is to improve automatic proof in specific problem domains where current automatic provers are weak or have blind spots.
For example, SMT solvers of the latest generation (e.g. CVC4, which is also used in the SPARK toolset), are very efficient when reasoning about linear arithmetic, but not so good when reasoning about non-linear arithmetic. Bitwise reasoning (also called bitvectors in the jargon of prover developers, available in e.g. CVC4) can be used to get better provability (for bitwise operations obviously, but also for other non-linear operations such as multiplication and division), but this seems to come with a cost in proving time for the linear case. The situation is somewhat worse for floating point operations, smart handling of these just being integrated into CVC4. Again with expected increased proof time for some goals, in exchange for better handling of specific operations on floating points.
Another family of provers, called constraint solvers, are quite efficient at reasoning about all kinds of data types including bitvectors and floating point operations, but are quite weak when it comes to boolean reasoning.
The aim of the SOPRANO project is to obtain better provability by combining the ideas of SMT solvers and constraint solvers. Head of the project is François Bobot from CEA. Other partners are various researchers from INRIA, the company OcamlPro which develops the SMT solver Alt-ergo, and AdaCore. For AdaCore, the potential benefit is obvious: If successful, the project will result in more proved VCs in the SPARK toolset, better counterexamples and overall easier handling of the tools.
The Kickoff Meeting of SOPRANO was held on Wednesday, Jan 15th 2015, at the CEA NanoInnov Building. There were a number of presentations that day:
- Guillaume Melquiond from INRIA presented the Gappa tool for reasoning about floating point operations;
- Evelyne Contejean from INRIA and Mohamed Iguernelala from OcamlPro and presented the past and the future of Alt-Ergo;
- Bruno Marre presented the constraint-based tools Gatel and Colibri for test case generation for Lustre programs;
- Mathieu Acher from Irisa presented a possible application of an efficient solver to the variability problem (problem of representing and reasoning about the variants of a system, e.g. a car with different options)
- Sébastian Bardin from CEA presented earlier work about bitwise reasoning using constraint solvers;
- François Bobot from CEA presented the principles of the new prover called Popop.
- Johannes Kanig from AdaCore (that's me!) presented the current challenges for provers in the SPARK toolset.
Interesting ideas were shared and good discussions took place. All in all a good beginning of the SOPRANO project.