Title :
A decision procedure for an extensional theory of arrays
Author :
Stump, Aaron ; Barrett, Clark W. ; Dill, David L. ; Levitt, Jeremy
Author_Institution :
Comput. Syst. Lab., Stanford Univ., CA, USA
Abstract :
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
Keywords :
arrays; data structures; decidability; formal verification; program diagnostics; theorem proving; array theory; automated theorem proving; correctness proof; decision procedure; extensional theory; formal verification; program analysis; Application software; Design automation; Equations; Formal verification; Laboratories; Libraries; Logic arrays;
Conference_Titel :
Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on
Conference_Location :
Boston, MA
Print_ISBN :
0-7695-1281-X
DOI :
10.1109/LICS.2001.932480
