DocumentCode :
3223085
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
fYear :
2001
fDate :
2001
Firstpage :
29
Lastpage :
37
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on
Conference_Location :
Boston, MA
ISSN :
1043-6871
Print_ISBN :
0-7695-1281-X
Type :
conf
DOI :
10.1109/LICS.2001.932480
Filename :
932480
Link To Document :
بازگشت