A decision procedure for an extensional theory of arrays

A. Stump, C. W. Barrett, D. L. Dill, J. Levitt

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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)
Title of host publicationProceedings - Symposium on Logic in Computer Science
Pages29-37
Number of pages9
StatePublished - 2001
Event16th Annual IEEE Symposium on Logic in Computer Science - Boston, MA, United States
Duration: Jun 16 2001Jun 19 2001

Other

Other16th Annual IEEE Symposium on Logic in Computer Science
CountryUnited States
CityBoston, MA
Period6/16/016/19/01

Fingerprint

Decision Procedures
Automated Theorem Proving
Program Analysis
Formal Verification

ASJC Scopus subject areas

  • Logic

Cite this

Stump, A., Barrett, C. W., Dill, D. L., & Levitt, J. (2001). A decision procedure for an extensional theory of arrays. In Proceedings - Symposium on Logic in Computer Science (pp. 29-37)

A decision procedure for an extensional theory of arrays. / Stump, A.; Barrett, C. W.; Dill, D. L.; Levitt, J.

Proceedings - Symposium on Logic in Computer Science. 2001. p. 29-37.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Stump, A, Barrett, CW, Dill, DL & Levitt, J 2001, A decision procedure for an extensional theory of arrays. in Proceedings - Symposium on Logic in Computer Science. pp. 29-37, 16th Annual IEEE Symposium on Logic in Computer Science, Boston, MA, United States, 6/16/01.
Stump A, Barrett CW, Dill DL, Levitt J. A decision procedure for an extensional theory of arrays. In Proceedings - Symposium on Logic in Computer Science. 2001. p. 29-37
Stump, A. ; Barrett, C. W. ; Dill, D. L. ; Levitt, J. / A decision procedure for an extensional theory of arrays. Proceedings - Symposium on Logic in Computer Science. 2001. pp. 29-37
@inproceedings{af86004ee3c14979871ca90da1f2ab52,
title = "A decision procedure for an extensional theory of arrays",
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.",
author = "A. Stump and Barrett, {C. W.} and Dill, {D. L.} and J. Levitt",
year = "2001",
language = "English (US)",
pages = "29--37",
booktitle = "Proceedings - Symposium on Logic in Computer Science",

}

TY - GEN

T1 - A decision procedure for an extensional theory of arrays

AU - Stump, A.

AU - Barrett, C. W.

AU - Dill, D. L.

AU - Levitt, J.

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0034858360&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0034858360&partnerID=8YFLogxK

M3 - Conference contribution

SP - 29

EP - 37

BT - Proceedings - Symposium on Logic in Computer Science

ER -