Boolector: an efficient SMT solver for bit-vectors and arrays. 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.

References in zbMATH (referenced in 19 articles )

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

  1. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  2. Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh: Symbolic trajectory evaluation for word-level verification: theory and implementation (2017)
  3. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  4. Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (2017)
  5. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  6. Inala, Jeevana Priya; Singh, Rohit; Solar-Lezama, Armando: Synthesis of domain specific CNF encoders for bit-vector solvers (2016)
  7. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  8. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  9. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: Deciding bit-vector formulas with mcsat (2016)
  10. Zhou, Min; He, Fei; Wang, Bow-Yaw; Gu, Ming; Sun, Jiaguang: Array theory of bounded elements and its applications (2014)
  11. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  12. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  13. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  14. Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo: Exploiting step semantics for efficient bounded model checking of asynchronous systems (2012)
  15. Järvisalo, Matti; Biere, Armin; Heule, Marijn J.H.: Simulating circuit-level simplifications on CNF (2012)
  16. Jovanović, Dejan; Barrett, Clark: Sharing is caring: combination of theories (2011)
  17. Soeken, Mathias; Wille, Robert; Drechsler, Rolf: Encoding OCL data types for SAT-based verification of UML/OCL models (2011)
  18. Marić, Filip; Janičić, Predrag: URBiVA: uniform reduction to bit-vector arithmetic (2010)
  19. Brummayer, Robert; Biere, Armin: Boolector: an efficient SMT solver for bit-vectors and arrays (2009) ioport

Further publications can be found at: