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 23 articles )

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

1 2 next

  1. Hyvärinen, Antti E.J.; Marescotti, Matteo; Alt, Leonardo; Sharygina, Natasha: Opensmt2: an SMT solver for multi-core and cloud computing (2016)
  2. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  3. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  4. 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)
  5. Hyvärinen, Antti E.J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
  6. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  7. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  8. Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha: Evolcheck: incremental upgrade checker for C (2013)
  9. Gao, Sicun; Kong, Soonho; Clarke, Edmund M.: Dreal: an SMT solver for nonlinear theories over the reals (2013)
  10. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  11. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation of a theory of arrays (2012)
  12. Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.: $\delta $-complete decision procedures for satisfiability over the reals (2012)
  13. Gupta, Ashutosh: Improved single pass algorithms for resolution proof reduction (2012)
  14. Järvisalo, Matti; Biere, Armin; Heule, Marijn J.H.: Simulating circuit-level simplifications on CNF (2012)
  15. Pulina, Luca; Tacchella, Armando: Challenging SMT solvers to verify neural networks (2012)
  16. Sery, Ondrej; Fedyukovich, Grigory; Sharygina, Natasha: FunFrog: bounded model checking with interpolation-based function summarization (2012) ioport
  17. Althaus, Ernst; Becker, Bernd; Dumitriu, Daniel; Kupferschmid, Stefan: Integration of an LP solver into interval constraint propagation (2011)
  18. Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: An interpolating sequent calculus for quantifier-free Presburger arithmetic (2011)
  19. 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)
  20. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Rewriting-based quantifier-free interpolation for a theory of arrays (2011)

1 2 next