A decision procedure for an extensional theory of arrays
Aaron Stump, Clark Barrett, David L. Dill, Jeremy R. Levitt · 2002
A decision procedure for a theory of arrays is of interest for applications in formal verification, program analysis and automated theorem proving. This paper presents a decision procedure for an extensional theory of arrays and proves it correct.