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:
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 array
Forschungs-