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.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Konnov, Igor; Veith, Helmut; Widder, Josef: What you always wanted to know about model checking of fault-tolerant distributed algorithms (2016)
- Koskinen, Eric; Yang, Junfeng: Reducing crash recoverability to reachability (2016)
- Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
- Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
- 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)
- Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
- Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel: Deciding floating-point logic with abstract conflict driven clause learning (2014)
- Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014)
- Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The mathsat5 SMT solver (2013)
- Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: A modular approach to maxsat modulo theories (2013)
- Karrenberg, Ralf; Košta, Marek; Sturm, Thomas: Presburger arithmetic in memory access optimization for data-parallel languages (2013)
Further publications can be found at: http://mathsat.fbk.eu/publications.html