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

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

1 2 next

  1. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  2. Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)
  3. Hyvärinen, Antti E. J.; Marescotti, Matteo; Alt, Leonardo; Sharygina, Natasha: Opensmt2: an SMT solver for multi-core and cloud computing (2016)
  4. Pham, Tuan-Hung; Gacek, Andrew; Whalen, Michael W.: Reasoning about algebraic data types with abstractions (2016)
  5. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  6. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  7. 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)
  8. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  9. Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
  10. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  11. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  12. Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha: eVolCheck: incremental upgrade checker for C (2013)
  13. Gao, Sicun; Kong, Soonho; Clarke, Edmund M.: dReal: an SMT solver for nonlinear theories over the reals (2013)
  14. Leino, K. Rustan M.: Automating theorem proving with SMT (2013)
  15. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation of a theory of arrays (2012)
  16. Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.: $\delta $-complete decision procedures for satisfiability over the reals (2012)
  17. Gupta, Ashutosh: Improved single pass algorithms for resolution proof reduction (2012)
  18. Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H.: Simulating circuit-level simplifications on CNF (2012)
  19. Pulina, Luca; Tacchella, Armando: Challenging SMT solvers to verify neural networks (2012)
  20. Sery, Ondrej; Fedyukovich, Grigory; Sharygina, Natasha: FunFrog: bounded model checking with interpolation-based function summarization (2012) ioport

1 2 next