Lemmas on Demand for the Extensional Theory of Arrays
Sprache des Vortragstitels:
Englisch
Original Kurzfassung:
Deciding satisfiability in the theory of arrays, particularly
in combination with bit-vectors, is essential for software and hardware
verification. We precisely describe how the lemmas on demand approach
can be applied to this decision problem. In particular, we show how our
new propagation based algorithm can be generalized to the extensional
theory of arrays. Our implementation achieves competitive performance.
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Vortrag auf einer Tagung (referiert)
Vortragsdatum:
08.07.2008
Vortragsort:
Vereinigte Staaten
Details zum Vortragsort:
SMT-COMP’08, Tool Presentation Princeton, New Jersey
Forschungs-