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:
Satisability Modulo Theories (SMT) is the problem of de-
ciding satisability 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 quantier-free theories
of bit-vectors and arrays. It uses term rewriting, bit-blasting to handle
bit-vectors, and lemmas on demand for array