• 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
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3223085