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

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

1 2 next

  1. Bromberger, Martin; Weidenbach, Christoph: New techniques for linear arithmetic: cubes and equalities (2017)
  2. 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)
  3. Chen, Li; Lyu, Yinrun; Wang, Chong; Wu, Jingzheng; Zhang, Changyou; Min-Allah, Nasro; Alhiyafi, Jamal; Wang, Yongji: Solving linear optimization over arithmetic constraint formula (2017)
  4. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  5. Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)
  6. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  7. Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas: \ssfSC$^2$: satisfiability checking meets symbolic computation. (Project paper) (2016)
  8. Bromberger, Martin; Weidenbach, Christoph: Fast cube tests for LIA constraint solving (2016)
  9. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano: Infinite-state invariant checking with IC3 and predicate abstraction (2016)
  10. Konnov, Igor; Veith, Helmut; Widder, Josef: What you always wanted to know about model checking of fault-tolerant distributed algorithms (2016)
  11. Koskinen, Eric; Yang, Junfeng: Reducing crash recoverability to reachability (2016)
  12. Kremer, Gereon; Corzilius, Florian; Ábrahám, Erika: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic (2016)
  13. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: Deciding bit-vector formulas with mcsat (2016)
  14. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  15. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  16. Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving (2015)
  17. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Proving correctness of imperative programs by linearizing constrained Horn clauses (2015)
  18. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  19. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  20. Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel: Deciding floating-point logic with abstract conflict driven clause learning (2014)

1 2 next


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