We present MATHSAT 4, a state-of-the-art SMT solver. MATHSAT 4 handles several useful theories: (combinations of) equality and uninterpreted functions, difference logic, linear arithmetic, and the theory of bit-vectors. It was explicitly designed for being used in formal verification, and thus provides functionalities which extend the applicability of SMT in this setting. In particular: model generation (for counterexample reconstruction), model enumeration (for predicate abstraction), an incremental interface (for BMC), and computation of unsatisfiable cores and Craig interpolants (for abstraction refinement). © 2008 Springer-Verlag.
CITATION STYLE
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., & Sebastiani, R. (2008). The MATHSAT 4 SMT solver: Tool paper. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5123 LNCS, pp. 299–303). https://doi.org/10.1007/978-3-540-70545-1_28
Mendeley helps you to discover research relevant for your work.