Robert Brummayer, Florian Lonsing, Armin Biere,
"Lemmas on Demand for the Extensional Theory of Arrays"
: Proc. 6th Intl. Workshop on Satisfiability Modulo Theories (SMT'08), 2008
Original Titel:
Lemmas on Demand for the Extensional Theory of Arrays
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 6th Intl. Workshop on Satisfiability Modulo Theories (SMT'08)
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.
Forschungs-