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.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
- Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
- Zhou, Min; He, Fei; Wang, Bow-Yaw; Gu, Ming; Sun, Jiaguang: Array theory of bounded elements and its applications (2014)
- Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013)
- Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
- Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
- Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo: Exploiting step semantics for efficient bounded model checking of asynchronous systems (2012)
- Järvisalo, Matti; Biere, Armin; Heule, Marijn J.H.: Simulating circuit-level simplifications on CNF (2012)
- Marić, Filip; Janičić, Predrag: URBiVA: uniform reduction to bit-vector arithmetic (2010)
- Brummayer, Robert; Biere, Armin: Boolector: an efficient SMT solver for bit-vectors and arrays (2009)
Further publications can be found at: http://fmv.jku.at/papers/index.html