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 56 articles , 1 standard article )

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

1 2 3 next

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Backeman, Peter; Rümmer, Philipp; Zeljić, Aleksandar: Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (2021)
  3. Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick: Optimization modulo non-linear arithmetic via incremental linearization (2021)
  4. Griggio, Alberto; Roveri, Marco; Tonetta, Stefano: Certifying proofs for SAT-based model checking (2021)
  5. Kruff, Niclas; Lüders, Christoph; Radulescu, Ovidiu; Sturm, Thomas; Walcher, Sebastian: Algorithmic reduction of biological networks with multiple time scales (2021)
  6. Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark Barrett: Pono: A Flexible and Extensible SMT-Based Model Checker (2021) not zbMATH
  7. Mann, Makai; Wilson, Amalee; Zohar, Yoni; Stuntz, Lindsey; Irfan, Ahmed; Brown, Kristopher; Donovick, Caleb; Guman, Allison; Tinelli, Cesare; Barrett, Clark: Smt-Switch: a solver-agnostic C++ API for SMT solving (2021)
  8. Wernhard, Christoph: Craig interpolation with clausal first-order tableaux (2021)
  9. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  10. Holík, Lukáš; Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš: Abstraction refinement and antichains for trace inclusion of infinite state systems (2020)
  11. Huang, Cheng-Chao; Xu, Ming; Li, Zhi-Bin: A conflict-driven solving procedure for poly-power constraints (2020)
  12. Rümmer, Philipp: Competition report: CHC-COMP-20 (2020)
  13. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  14. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
  15. Bromberger, Martin; Fleury, Mathias; Schwarz, Simon; Weidenbach, Christoph: SPASS-SATT. A CDCL(LA) solver (2019)
  16. Dietsch, Daniel; Heizmann, Matthias; Hoenicke, Jochen; Nutz, Alexander; Podelski, Andreas: Ultimate TreeAutomizer (CHC-COMP tool description) (2019)
  17. Vyskocil, Tomas; Djidjev, Hristo: Embedding equality constraints of optimization problems into a quantum annealer (2019)
  18. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  19. Brandl, Florian; Brandt, Felix; Eberl, Manuel; Geist, Christian: Proving the incompatibility of efficiency and strategyproofness via SMT solving (2018)
  20. Bromberger, Martin: A reduction from unbounded linear mixed arithmetic problems into bounded problems (2018)

1 2 3 next


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