The OpenSMT solver. This paper describes OpenSMT, an incremental, efficient, and open-source SMT-solver. OpenSMT has been specifically designed to be easily extended with new theory-solvers, in order to be accessible for non-experts for the development of customized algorithms. We sketch the solver’s architecture and interface. We discuss its distinguishing features w.r.t. other state-of-the-art solvers.

References in zbMATH (referenced in 21 articles )

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

1 2 next

  1. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  2. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  3. Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving (2015)
  4. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  5. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  6. Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha: Evolcheck: incremental upgrade checker for C (2013)
  7. Gao, Sicun; Kong, Soonho; Clarke, Edmund M.: Dreal: an SMT solver for nonlinear theories over the reals (2013)
  8. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  9. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation of a theory of arrays (2012)
  10. Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.: $\delta $-complete decision procedures for satisfiability over the reals (2012)
  11. Gupta, Ashutosh: Improved single pass algorithms for resolution proof reduction (2012)
  12. Järvisalo, Matti; Biere, Armin; Heule, Marijn J.H.: Simulating circuit-level simplifications on CNF (2012)
  13. Pulina, Luca; Tacchella, Armando: Challenging SMT solvers to verify neural networks (2012)
  14. Sery, Ondrej; Fedyukovich, Grigory; Sharygina, Natasha: Funfrog: bounded model checking with interpolation-based function summarization (2012)
  15. Althaus, Ernst; Becker, Bernd; Dumitriu, Daniel; Kupferschmid, Stefan: Integration of an LP solver into interval constraint propagation (2011)
  16. Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: An interpolating sequent calculus for quantifier-free Presburger arithmetic (2011)
  17. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Rewriting-based quantifier-free interpolation for a theory of arrays (2011)
  18. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints (2011)
  19. Loup, Ulrich; Ábrahám, Erika: I-RiSC: an SMT-compliant solver for the existential fragment of real algebra (2011)
  20. Bruttomesso, Roberto; Pek, Edgar; Sharygina, Natasha; Tsitovich, Aliaksei: The OpenSMT solver (2010)

1 2 next