Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver.
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
This paper shows how all different constraints
(ADCs) over bit-vectors can be handled within a SAT solver.
It also contains encouraging experimental results in applying
this technique to encode simple path constraints in bounded
model checking. Finally, we present a new compact encoding
of equalities and inequalities over bit-vectors in CNF
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Vortrag auf einer Tagung (referiert)
Vortragsdatum:
18.11.2008
Vortragsort:
Vereinigte Staaten
Details zum Vortragsort:
8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08) Portland, Oregon
Forschungs-