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

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

1 2 next

  1. Asăvoae, Irina Măriuca; Shirazi, Ramtine Tofighi; Riesco, Adrián; Yasuyoshi, Uemura: Hardware Trojan detection via rewriting logic (2022)
  2. Mann, Makai; Wilson, Amalee; Zohar, Yoni; Stuntz, Lindsey; Irfan, Ahmed; Brown, Kristopher; Donovick, Caleb; Guman, Allison; Tinelli, Cesare; Barrett, Clark: Smt-Switch: a solver-agnostic C++ API for SMT solving (2021)
  3. Trentin, Patrick; Sebastiani, Roberto: Optimization modulo the theories of signed bit-vectors and floating-point numbers (2021)
  4. Jonáš, Martin; Strejček, Jan: Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions (2020)
  5. Bueno, Denis; Sakallah, Karem A.: EUFORIA: complete software model checking with uninterpreted functions (2019)
  6. Trentin, Patrick; Sebastiani, Roberto: Optimization modulo the theory of floating-point numbers (2019)
  7. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  8. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  9. Ge, Cunjing; Ma, Feifei; Liu, Tian; Zhang, Jian; Ma, Xutong: A new probabilistic algorithm for approximate model counting (2018)
  10. Niewiadomski, Artur; Switalski, Piotr; Sidoruk, Teofil; Penczek, Wojciech: SMT-solvers in action: encoding and solving selected problems in NP and EXPTIME (2018)
  11. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  12. 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)
  13. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  14. Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (2017)
  15. Preiner, Mathias; Niemetz, Aina; Biere, Armin: Counterexample-guided model synthesis (2017)
  16. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  17. Surynek, Pavel: Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems (2017)
  18. Inala, Jeevana Priya; Singh, Rohit; Solar-Lezama, Armando: Synthesis of domain specific CNF encoders for bit-vector solvers (2016)
  19. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  20. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)

1 2 next

Further publications can be found at: