Activity: Talk or presentation › Contributed talk › unknown
Description
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.