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 48 articles , 1 standard article )

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

1 2 3 next

  1. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  2. Teso, Stefano; Sebastiani, Roberto; Passerini, Andrea: Structured learning modulo theories (2017)
  3. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  4. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  5. Sebastiani, Roberto; Tomasi, Silvia: Optimization modulo theories with linear rational costs (2015)
  6. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
  7. Dräger, Klaus; Kwiatkowska, Marta; Parker, David; Qu, Hongyang: Local abstraction refinement for probabilistic timed programs (2014)
  8. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  9. 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) ioport
  10. Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The MathSAT5 SMT solver (2013)
  11. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: SMT-based scenario verification for hybrid systems (2013)
  12. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  13. Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
  14. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  15. Zhan, Naijun; Wang, Shuling; Zhao, Hengjun: Formal modelling, analysis and verification of hybrid systems (2013)
  16. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: From under-approximations to over-approximations and back (2012)
  17. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: Whale: an interpolation-based algorithm for inter-procedural verification (2012)
  18. Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving constraint satisfaction problems with SAT modulo theories (2012)
  19. 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)
  20. Järvisalo, Matti; Biere, Armin; Heule, Marijn J.H.: Simulating circuit-level simplifications on CNF (2012)

1 2 3 next