Abstract
Satisfiability Modulo Theories (SMT) is the problem of deciding satisfiability of a logical formula, expressed in a combination of first-order theories. We present the architecture and selected features of Boolector, which is an efficient SMT solver for the quantifier-free theories of bit-vectors and arrays. It uses term rewriting, bit-blasting to handle bit-vectors, and lemmas on demand for arrays.
Chapter PDF
Similar content being viewed by others
References
Babic, D.: Exploiting Structure for Scalable Software Verification. PhD thesis (2008)
Barrett, C., Deters, M., Oliveras, A., Stump, A.: SMT-Comp. (2008), http://www.smtcomp.org
Biere, A.: PicoSAT essentials. JSAT 4 (2008)
Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)
Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. In: Proc. SMT (2008)
Brummayer, R., Biere, A., Lonsing, F.: BTOR: Bit-precise modelling of word-level problems for model checking. In: Proc. BPR (2008)
Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1–26. Springer, Heidelberg (2008)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Proc. SAT (2002)
Kroening, D., Strichman, O.: Decision Procedures: An algorithmic Point of View. Springer, Heidelberg (2008)
Ranise, S., Tinelli, C.: The satisfiability modulo theories library, SMT-LIB (2008), http://www.smt-lib.org
Sebastiani, R.: Lazy satisfiability modulo theories. JSAT, 3 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brummayer, R., Biere, A. (2009). Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2009. Lecture Notes in Computer Science, vol 5505. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00768-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-00768-2_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00767-5
Online ISBN: 978-3-642-00768-2
eBook Packages: Computer ScienceComputer Science (R0)