SMArT // Satisfiability Modulo Arithmetic and Theories

• Applicant: Dr. Michael Sagraloff, since 3/2016
• Subject Area: Theoretical Computer Science
• Term: from 2013 to 2018
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 242816019

The project aims to make advanced techniques for arithmetic reasoning available to formal system verification. During the last decade, there has been tremendous progress on symbolic verification techniques, spurred in particular by the development of SMT solvers, which are successfully used for program verification, bounded and parameterized model checking, test generation, etc. They combine a SAT solver with theory reasoners for deciding satisfiability of sets of literals over interpreted symbols, and instantiation techniques for handling quantifiers.Reasoning in fragments of arithmetic is a fundamental requirement in verification. By arithmetic we mean any theory whose language includes functions 0, 1, +, *, but possibly also mod, sin, exp etc., interpreted over integer, rational, real or complex numbers or a mix of those. There are well-known results on the decidability and complexity of fragments of arithmetic that impose strict limits on the capabilities of automatic tools. For many practical applications it is, however, enough to handle restricted subsets of arithmetic.Today's SMT solvers are mostly limited to quantifier-free formulas over linear arithmetic. This is sufficient for ensuring properties such as the absence of out-of-bound array accesses in simple heap-manipulating programs. Nevertheless, this severely restricts expressiveness. Ideas have emerged to support stronger arithmetic fragments. These ideas are interesting but limited in scope and efficiency as they mostly ignore existing work.Instead, we propose to adapt within an SMT context known efficient techniques and algorithms for which mature solvers exist. The advantages are: (1) the arithmetic solver need not handle propositional operators, (2) the SMT solver gets access to a sophisticated infrastructure for handling expressive arithmetic fragments, (3) users benefit from the modular architecture of SMT solvers where arithmetic can be combined with other relevant theories.Such an integration requires foundational work on the existing procedures for arithmetic including the generation of models and unsatisfiable cores or the computation of implied equalities. Conversely, an efficient integration of non-linear arithmetic requires loosening some conceptual assumptions that SMT solvers make: the theory is not convex, nor is it disjoint when the linear case is handled by a dedicated theory reasoner.Our techniques will be implemented in a solver that integrates Redlog, an efficient and mature solver for non-linear arithmetic, and veriT, a state-of-the-art SMT solver. This integration will be made available as an open source implementation, under a permissive license. We will evaluate the project results using benchmark problems from the Rodin and TLAPS platforms and non-linear problems in the SMT-LIB repository. Key developers of these platforms are partners in the project consortium.

• DFG Programme: Research Grants
• International Connection: France
• Partner Organisation: Agence Nationale de la Recherche / The French National Research Agency
• Participating Person: Professor Dr. Pascal Fontaine
• Ehemaliger Antragsteller: Privatdozent Dr. Thomas Sturm, until 3/2016