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.
|Original language||English (US)|
|Number of pages||9|
|Journal||Proceedings - Symposium on Logic in Computer Science|
|State||Published - Jan 1 2001|
ASJC Scopus subject areas