{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T19:07:18Z","timestamp":1775329638707,"version":"3.50.1"},"reference-count":15,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2001.932480","type":"proceedings-article","created":{"date-parts":[[2002,11,13]],"date-time":"2002-11-13T16:02:21Z","timestamp":1037203341000},"page":"29-37","source":"Crossref","is-referenced-by-count":56,"title":["A decision procedure for an extensional theory of arrays"],"prefix":"10.1109","author":[{"given":"A.","family":"Stump","sequence":"first","affiliation":[]},{"given":"C.W.","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"D.L.","family":"Dill","sequence":"additional","affiliation":[]},{"given":"J.","family":"Levitt","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"ref11","first-page":"748","article-title":"PVS: A Prototype Verification System","author":"owre","year":"1992","journal-title":"11 th International Conference on Automated Deduction volume 607 of Lecture Notes in Artificial Intelligence"},{"key":"ref12","author":"ruess","year":"2000","journal-title":"private communication"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"ref14","article-title":"On a Very Simple Abstract Higher-Order Congruence Closure Algorithm","author":"stump","year":"2000"},{"key":"ref15","article-title":"Verification Decidability of Presburger Array Programs","author":"suzuki","year":"1977","journal-title":"Proceedings of a Conference on Theoretical Computer Science"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/322092.322104"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60275-5_61"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/321439.321447"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"ref8","article-title":"Towards a Mathematical Science of Computation","author":"mccarthy","year":"1962","journal-title":"IFIP Congress 62"},{"key":"ref7","author":"levitt","year":"1999","journal-title":"Formal Verification Techniques for Digital Systems"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_6"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/10721959_5","article-title":"Abstract Congruence Closure and Specializations","volume":"1831","author":"bachmair","year":"2000","journal-title":"17th International Conference on Automated Deduction"},{"key":"ref9","article-title":"Techniques for Program Verification","author":"nelson","year":"1981","journal-title":"Technical Report CSL-81-10"}],"event":{"name":"16th Annual IEEE Symposium on Logic in Computer Science","location":"Boston, MA, USA","acronym":"LICS-01"},"container-title":["Proceedings 16th Annual IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/7424\/20180\/00932480.pdf?arnumber=932480","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,11]],"date-time":"2020-03-11T08:35:26Z","timestamp":1583915726000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/932480\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":15,"URL":"https:\/\/doi.org\/10.1109\/lics.2001.932480","relation":{},"subject":[]}}