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. © 2013 Springer-Verlag.
CITATION STYLE
Cimatti, A., Griggio, A., Schaafsma, B. J., & Sebastiani, R. (2013). The MathSAT5 SMT solver. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7795 LNCS, pp. 93–107). https://doi.org/10.1007/978-3-642-36742-7_7
Mendeley helps you to discover research relevant for your work.