Abstract
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.
Chapter PDF
Similar content being viewed by others
References
SMT-COMP, http://www.smtcomp.org
Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories. In: Handbook on Satisfiability, vol. 185. IO Press (2009)
Bruttomesso, R.: An Extension of the Davis-Putnam Procedure and its Application to Preprocessing in SMT. In: SMT (2009)
Bruttomesso, R., Sharygina, N.: A Scalable Decision Procedure for Fixed-Width Bit-Vectors. In: ICCAD (2009)
Cotton, S., Maler, O.: Fast and Flexible Difference Constraint Propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of ACM 52(3), 365–473 (2005)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions. In: ESEC/FSE, pp. 23–32 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A. (2010). The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)