A decision procedure for an extensional theory of arrays

Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy Levitt

Research output: Contribution to journalArticle

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.

Original languageEnglish (US)
Pages (from-to)29-37
Number of pages9
JournalProceedings - Symposium on Logic in Computer Science
DOIs
StatePublished - Jan 1 2001

    Fingerprint

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Cite this