SMArT // Satisfiability Modulo Arithmetic and Theories
Final Report Abstract
SMArT is an bilateral research project supported by ANR and DFG. Arithmetic, a Limitation for Verification. Reasoning in various fragments of arithmetic is a fundamental and ubiquitous requirement in verification. In our context, by arithmetic we mean any theory whose language includes equations and inequalities with terms in rational numbers, addition, and multiplication possibly supplemented with further functions, e.g., mod, exponentiation, trigonometric functions. Logical combinations, using the common connectives of propositional logic but also quantifiers ∃x “there exists an x such that” and ∀x “for all x”, are interpreted over various domains ranging from the integers Z to the complex numbers C or even a mix of those. There are well-known fundamental results about the decidability (and then complexity) and undecidability of arithmetic in our sense that impose strict limits on the capabilities of automatic tools. For many practical applications, it is, however, sufficient to consider restricted fragments of arithmetic. Satisfiability Moduls Theories (SMT) solvers combine successful SAT-solving approaches on the propositional side with specialized arithmetic theory solvers on the algebraic side. Today’s SMT solvers are mostly limited to quantifier-free formulas over linear arithmetic (i.e., formulas involving only rational numbers and addition), for which efficient decision procedures exist over both integers 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. While these ideas are interesting, they mostly ignore existing work on reasoning in non-linear arithmetic and are limited in scope and efficiency. Cooperation, Integration, Specialization of State-of-the-art Methods and Tools. SMArT adapts existing efficient techniques and algorithms, for which mature solvers exist, so that they can be used within an SMT context. This has several advantages: (1) The arithmetic solver need not deal with propositional logic anymore. (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. Such an integration requires foundational work on (semi-)decision procedures for arithmetic, and on their integration in an SMT framework, including the generation of models in the satisfiable case, of unsatisfiable cores otherwise, 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. Main Results and Impact. In addition to significant foundational contributions, we have realized the major part of our results in software, which allows to assess their applicability and relevance. Our techniques are implemented in a solver that integrates Redlog, an efficient and mature solver for nonlinear arithmetic (developed by the German project coordinator), and veriT, a state-of-the-art SMT solver (developed by the French project coordinator). This combined product is available open-source, under a permissive license. We hope that it will be used in verification platforms and that the academic community will improve upon it in the future. We have quantitatively evaluated the project results by applying the solver to benchmark problems stemming from the Rodin and TLAPS platforms, and over non-linear problems in the SMT-LIB repository. Key developers of these platforms are industrial and academic partners in the project consortium. Presentation and publication of SMArT results in the originally separate scientific communities of Satisfiability Checking and Symbolic Computation has triggered significant exchange and cooperation between those communities, which culminated in a successful Horizon 2020 EU project SC2 (Satisfiability Checking and Symbolic Computation, 2016–2018), where French and German SMArT coordinators took an active role on the consortium.
Publications
- Towards Conflict-Driven Learning for Virtual Substitution. Proc. CASC 2014, LNCS 8660, pp.256–270, Sep 2014
K. Korovin, M. Košta, and T. Sturm
(See online at https://doi.org/10.1007/978-3-319-10515-4_19) - Adapting Real Quantifier Elimination Methods for Conflict Set Computation. Proc. FROCOS 2016, LNCS 9322, pp.151–166, Nov 2015
M. Jaroschek, P. F. Dobal, and P. Fontaine
(See online at https://doi.org/10.1007/978-3-319-24246-0_10) - Linear Integer Arithmetic Revisited. Proc. CADE-25, LNCS 9195, pp.623–637, Oct 2015
M. Bromberger, T. Sturm, and C. Weidenbach
(See online at https://doi.org/10.1007/978-3-319-21401-6_42) - Better Answers to Real Questions. J. Symb. Comput., 74:255– 275, May 2016
M. Košta, T. Sturm, and A. Dolzmann
(See online at https://doi.org/10.1016/j.jsc.2015.07.002) - SC2 : Satisfiability Checking Meets Symbolic Computation. Proc. CICM 2016, LNCS 9791, pp.28–43, Nov 2016
E. Abraham, J. Abbott, B. Becker, A. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. Davenport, M. England, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. Seiler, and T. Sturm
(See online at https://doi.org/10.1007/978-3-319-42547-4_3) - Subtropical Satisfiability. Proc. FROCOS 2017, LNCS 10483, pp.189–206, Sep 2017
P. Fontaine, M. Ogawa, T. Sturm, and X. T. Vu
(See online at https://doi.org/10.1007/978-3-319-66167-4_11)
