Paper: A Decision Procedure for an Extensional Theory of Arrays (at LICS 2001)
Authors: Aaron Stump Clark W. Barrett David L. Dill Jeremy LevittAbstract
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.
BibTeX
@InProceedings{StumpBarrettDillLev-ADecisionProceduref, author = {Aaron Stump and Clark W. Barrett and David L. Dill and Jeremy Levitt}, title = {A Decision Procedure for an Extensional Theory of Arrays}, booktitle = {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001}, year = 2001, editor = {Joseph Halpern}, month = {June}, pages = {29--37}, location = {Boston, MA, USA}, publisher = {IEEE Computer Society Press} }