Boolector: An Effcient SMT Solver for Bit-Vectors and Arrays
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
TACAS'09 Conference
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Satis ability Modulo Theories (SMT) is the problem of de-
ciding satis ability of a logical formula, expressed in a combination of
rst-order theories. We present the architecture and selected features of
Boolector, which is an ecient SMT solver for the quanti er-free theories
of bit-vectors and arrays. It uses term rewriting, bit-blasting to handle
bit-vectors, and lemmas on demand for array
Forschungs-