MathSAT

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

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

1 2 3 next

  1. Geatti, Luca; Gigante, Nicola; Montanari, Angelo: A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL (2019)
  2. Morettin, Paolo; Passerini, Andrea; Sebastiani, Roberto: Advanced SMT techniques for weighted model integration (2019)
  3. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions (2018)
  4. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  5. Teso, Stefano; Sebastiani, Roberto; Passerini, Andrea: Structured learning modulo theories (2017)
  6. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  7. Barrett, Clark; de Moura, Leonardo; Fontaine, Pascal: Proofs in satisfiability modulo theories (2015)
  8. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  9. Sebastiani, Roberto; Tomasi, Silvia: Optimization modulo theories with linear rational costs (2015)
  10. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
  11. Dräger, Klaus; Kwiatkowska, Marta; Parker, David; Qu, Hongyang: Local abstraction refinement for probabilistic timed programs (2014)
  12. Phan, Quoc-Sang: Symbolic execution as DPLL modulo theories (2014)
  13. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  14. 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
  15. Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The MathSAT5 SMT solver (2013)
  16. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: SMT-based scenario verification for hybrid systems (2013)
  17. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  18. Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
  19. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  20. Zhan, Naijun; Wang, Shuling; Zhao, Hengjun: Formal modelling, analysis and verification of hybrid systems (2013)

1 2 3 next