The MathSAT 4 SMT Solver. 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).

References in zbMATH (referenced in 39 articles , 1 standard article )

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

1 2 next

  1. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  2. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
  3. Dräger, Klaus; Kwiatkowska, Marta; Parker, David; Qu, Hongyang: Local abstraction refinement for probabilistic timed programs (2014)
  4. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  5. Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Leonardsson, Carl; Rezine, Ahmed: Memorax, a precise and sound tool for automatic fence insertion under TSO (2013)
  6. Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The mathsat5 SMT solver (2013)
  7. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: SMT-based scenario verification for hybrid systems (2013)
  8. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  9. Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
  10. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  11. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: From under-approximations to over-approximations and back (2012)
  12. Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving constraint satisfaction problems with SAT modulo theories (2012)
  13. Damm, Werner; Dierks, Henning; Disch, Stefan; Hagemann, Willem; Pigorsch, Florian; Scholl, Christoph; Waldmann, Uwe; Wirtz, Boris: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces (2012)
  14. Järvisalo, Matti; Biere, Armin; Heule, Marijn J.H.: Simulating circuit-level simplifications on CNF (2012)
  15. Rintanen, Jussi: Planning as satisfiability: heuristics (2012)
  16. Althaus, Ernst; Becker, Bernd; Dumitriu, Daniel; Kupferschmid, Stefan: Integration of an LP solver into interval constraint propagation (2011)
  17. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Boosting lazy abstraction for SystemC with partial order reduction (2011)
  18. Griggio, Alberto; Phan, Quoc-Sang; Sebastiani, Roberto; Tomasi, Silvia: Stochastic local search for SMT: combining theory solvers with WalkSAT (2011)
  19. Haarslev, Volker; Sebastiani, Roberto; Vescovi, Michele: Automated reasoning in $\mathcalALCQ$ via SMT (2011)
  20. Jovanović, Dejan; Barrett, Clark: Sharing is caring: combination of theories (2011)

1 2 next