The objective of the SMArT project is to provide advanced techniques for arithmetic reasoning for formal system verification. During the last decade, there has been tremendous progress on symbolic verification techniques, spurred in particular by the development of SMT (satisfiability modulo theories) techniques and tools. SMT solvers are core engines that are successfully used for program verification, bounded and parameterized model checking, test generation, etc. They combine a SAT solver for deciding satisfiability of propositional logic with theory reasoners for deciding satisfiability of sets of literals over interpreted symbols, and instantiation techniques for handling quantifiers.
Reasoning in various fragments of arithmetic is a fundamental and ubiquitous requirement in verification. Today's SMT solvers are mostly limited to quantifier-free formulas over linear arithmetic (i.e., formulas involving only constants, +, and <), for which efficient decision procedures exist over both integer and real numbers. This fragment is sufficient for ensuring certain properties such as the absence of out-of-bound array accesses in simple heap-manipulating programs. Nevertheless, the linear fragment represents a severe restriction on expressiveness, and ideas have started to emerge on the support for stronger arithmetic fragments within SMT solvers.
We propose to adapt known efficient techniques and algorithms to handle rich arithmetic fragments and for which mature solvers exist, so that they can be used within an SMT context. The advantages of such a combination are: (1) the arithmetic solver no longer needs to handle propositional operators, (2) the SMT solver gets access to a sophisticated infrastructure (data structures and algorithms) for handling much more expressive arithmetic fragments, (3) users benefit from the modular architecture of SMT solvers where arithmetic can be combined with other relevant theories.
[21/09/15] A prototype version of veriT running with Redlog is available here. The software has been tested on the QF_NRA category of the SMT-LIB and results are promising. You might experience some difficulties to compile though. We are working hard to improve performance, expressiveness, and the compilation procedure. Stay tuned!
[26/01/15] P. Fontaine and T. Sturm (coordinators of this project) are co-organizing (with Erika Abraham and Dongming Wang) a Dagstuhl seminar in Nov. 2015 on Symbolic Computation and Satisfiability Checking
[13/11/14] Fifth meeting: the JAIST-Loria Workshop 2014 on SMT
[01/09/14] Pablo Federico Dobal is becoming a PhD Student in Nancy in the project
[04/08/14] The SMArT Summer School will take place at MPI from August 04 to August 08.
[01/07/14] Maximilian Jaroschek is joining MPI as a PostDoc in the project
[13/06/14] The next meeting is planned in Vienna on July 17-18 2014, in the Vienna Summer of Logic
[12/06/14] Second meeting
[06/05/14] Kick-off meeting
[01/12/13] Haniel Barbosa is joining the team in Nancy as a PhD Student
[21/10/13] The ANR-DFG project SMArT has been accepted