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

Showing results 1 to 20 of 28.
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. Abraham, Erika: Building bridges between symbolic computation and satisfiability checking (2015)
  6. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  7. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  8. Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: \textttSMT-RAT: an open source \textttC++ toolbox for strategic and parallel SMT solving (2015)
  9. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  10. Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
  11. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  12. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  13. Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha: eVolCheck: incremental upgrade checker for C (2013)
  14. Gao, Sicun; Kong, Soonho; Clarke, Edmund M.: dReal: an SMT solver for nonlinear theories over the reals (2013)
  15. Leino, K. Rustan M.: Automating theorem proving with SMT (2013)
  16. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation of a theory of arrays (2012)
  17. Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.: (\delta)-complete decision procedures for satisfiability over the reals (2012)
  18. Gupta, Ashutosh: Improved single pass algorithms for resolution proof reduction (2012)
  19. Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H.: Simulating circuit-level simplifications on CNF (2012)
  20. Pulina, Luca; Tacchella, Armando: Challenging SMT solvers to verify neural networks (2012)

1 2 next