The MathSAT5 SMT Solver

By A. Cimatti, Alberto Griggio, B. Schaafsma, Roberto Sebastiani. International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2013

563 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Fuzzing: A Survey for Roadmap (2022, background): “, MathSAT5 [49] or Z3 [54]) are utilized to solve the path constraints.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “OMT is already supported by several solvers including MathSAT [46] and Z3. cvc5 already has internal infrastructure for supporting OMT queries.”
The nuXmv Symbolic Model Checker (2014, methodology): “For IC3 based algorithms, a more tight integration with the SMT solver is required, therefore we implemented them directly on top of MATHSAT5.”
Synthesizing coupling proofs of differential privacy (2017, methodology): “ean predicate abstraction, which requires exponentially many smt calls in the size of the predicates. To do so efficiently, we use the AllSMT algorithm of Lahiri et al. [32] in the MathSAT5smt solver [17]. Handling non-linearity. Observe that in the definition of shift couplings (Definition 3.6), th”
A Storm is Coming: A Modern Probabilistic Model Checker (2017, unknown): “SMT Z3 [46], MathSAT [47], SMTLIB [48] 4 Evaluation Set-up.”
Proving differential privacy with shadow execution (2019, methodology): “Also, CPAChecker has multiple solver backends such as MathSat [16], Z3 [17] and SMTInterpol [15].”