Robert Brummayer, Armin Biere,
"Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays"
: Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09), Serie Lecture Notes in Computer Science (LNCS), Vol. 5505, Springer, Seite(n) 174-177, 2009
Original Titel:
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09)
Original Kurzfassung:
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.
Forschungs-