MathSAT5

The mathsat5 SMT solver. MathSAT is a long-term project, which has been jointly carried on by FBK-IRST and University of Trento, with the aim of developing and maintaining a state-of-the-art SMT tool for formal verification (and other applications). MathSAT5 is the latest version of the tool. It supports most of the SMT-LIB theories and their combinations, and provides many functionalities (like e.g., unsat cores, interpolation, AllSMT). MathSAT5 improves its predecessor MathSAT4 in many ways, also providing novel features: first, a much improved incrementality support, which is vital in SMT applications; second, a full support for the theories of arrays and floating point; third, sound SAT-style Boolean formula preprocessing for SMT formulae; finally, a framework allowing users for plugging their custom tuned SAT solvers. MathSAT5 is freely available, and it is used in numerous internal projects, as well as by a number of industrial partners.


References in zbMATH (referenced in 45 articles , 1 standard article )

Showing results 1 to 20 of 45.
Sorted by year (citations)

1 2 3 next

  1. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  2. Holík, Lukáš; Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš: Abstraction refinement and antichains for trace inclusion of infinite state systems (2020)
  3. Huang, Cheng-Chao; Xu, Ming; Li, Zhi-Bin: A conflict-driven solving procedure for poly-power constraints (2020)
  4. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  5. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
  6. Bromberger, Martin; Fleury, Mathias; Schwarz, Simon; Weidenbach, Christoph: SPASS-SATT. A CDCL(LA) solver (2019)
  7. Vyskocil, Tomas; Djidjev, Hristo: Embedding equality constraints of optimization problems into a quantum annealer (2019)
  8. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  9. Brandl, Florian; Brandt, Felix; Eberl, Manuel; Geist, Christian: Proving the incompatibility of efficiency and strategyproofness via SMT solving (2018)
  10. Bromberger, Martin: A reduction from unbounded linear mixed arithmetic problems into bounded problems (2018)
  11. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  12. Cimatti, Alessandro; Do, Minh; Micheli, Andrea; Roveri, Marco; Smith, David E.: Strong temporal planning with uncontrollable durations (2018)
  13. Giunchiglia, Enrico; Maratea, Marco; Pulina, Luca: Translation-based approaches for solving disjunctive temporal problems with preferences (2018)
  14. Hong, Hoon; Sturm, Thomas: Positive solutions of systems of signed parametric polynomial inequalities (2018)
  15. Kremer, Gereon; Ábrahám, Erika: Modular strategic SMT solving with \textbfSMT-RAT (2018)
  16. Lvov, M.; Peschanenko, V.; Letychevskyi, O.; Tarasich, Y.; Baiev, A.: Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (2018)
  17. Niewiadomski, Artur; Switalski, Piotr; Sidoruk, Teofil; Penczek, Wojciech: SMT-solvers in action: encoding and solving selected problems in NP and EXPTIME (2018)
  18. Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp: Exploring approximations for floating-point arithmetic using uppsat (2018)
  19. Bromberger, Martin; Weidenbach, Christoph: New techniques for linear arithmetic: cubes and equalities (2017)
  20. Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh: Symbolic trajectory evaluation for word-level verification: theory and implementation (2017)

1 2 3 next


Further publications can be found at: http://mathsat.fbk.eu/publications.html