{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:11:42Z","timestamp":1774987902261,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T00:00:00Z","timestamp":1196467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2007,12]]},"abstract":"<jats:p>Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models containing first-order state variables, where the system state includes mutable functions and predicates. Such a model can describe systems containing arbitrarily large memories, buffers, and arrays of identical processes. We describe a form of predicate abstraction that constructs a formula over a set of universally quantified variables to describe invariant properties of the first-order state variables. We provide a formal justification of the soundness of our approach and describe how it has been used to verify several hardware and software designs, including a directory-based cache coherence protocol.<\/jats:p>","DOI":"10.1145\/1297658.1297662","type":"journal-article","created":{"date-parts":[[2007,12,21]],"date-time":"2007-12-21T14:52:36Z","timestamp":1198248756000},"page":"4","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Predicate abstraction with indexed predicates"],"prefix":"10.1145","volume":"9","author":[{"given":"Shuvendu K.","family":"Lahiri","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]},{"given":"Randal E.","family":"Bryant","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]}],"member":"320","published-online":{"date-parts":[[2007,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Conference on VLSI Design Conference (VLSI).","author":"Arons T."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Conference on Computer-Aided Verification (CAV), G. Berry, H. Comon, and A. Finkel, Eds. Lecture Notes in Computer Science","volume":"2102","author":"Arons T."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378846"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/646541.696180"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 1997. The Classical Decision Problem. Springer-Verlag.  B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 1997. The Classical Decision Problem. Springer-Verlag.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_2_1_7_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"1855","author":"Bouajjani A."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Workshop on Constraints in Formal Verification (CFV).","author":"Bryant R. E."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science","volume":"2404","author":"Bryant R. E."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.735662"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the International Conference on Software Engineering (ICSE). IEEE Computer Society, 385--395","author":"Chaki S."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143235"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_15_1","volume-title":"IEEE Symposium on Logic in Computer Science(LICS). IEEE Computer Society.","author":"Das S."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science","volume":"1633","author":"Das S."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), M. D. Aagaard and J. W. O'Leary, Eds. Lecture Notes in Computer Science","volume":"2517","author":"Das S."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the International Conference on Automated Deduction, D. A. McAllester, Ed.","author":"Emerson E. A.","year":"1831"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the international Conference on Correct Hardware Design and Verification Methods (CHARME), D. Geist and E. Tronci, Eds. Lecture Notes in Computer Science","volume":"2860","author":"Emerson E. A."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199468"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_23_1","unstructured":"German S. Personal communication.  German S. Personal communication."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the international Conference on Computer-Aided Verification (CAV), O. Grumberg, Ed. Lecture Notes in Computer Science","volume":"1254","author":"Graf S."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the international Conference on Computer-Aided Verification (CAV). LNCS.","author":"Hosabettu R."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV), R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science","volume":"1102","author":"Ip C. N."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV '97)","volume":"1254","author":"Kesten Y."},{"key":"e_1_2_1_30_1","unstructured":"Lahiri S. K. 2004. Unbounded system verification using decision procedures and predicate abstraction. PhD thesis Carnegie Mellon University.   Lahiri S. K. 2004. Unbounded system verification using decision procedures and predicate abstraction. PhD thesis Carnegie Mellon University."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), G. Levi and B. Steffen, Eds. Lecture Notes in Computer Science","volume":"2937","author":"Lahiri S. K."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV). To appear.","author":"Lahiri S. K."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV), W. A. Hunt, Jr. and F. Somenzi, Eds. Lecture Notes in Computer Science","volume":"2725","author":"Lahiri S. K."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), J. W. O. M. Aagaard, Ed. Lecture Notes in Computer Science","volume":"2517","author":"Lahiri S. K."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733764"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV), A. Emerson and P. Sistla, Eds. Lecture Notes in Computer Science","volume":"1855","author":"McMillan K."},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Perkins C. Royer E. and Das S. 2002. Ad hoc on demand distance vector (aodv) routing. In IETF Draft. http:\/\/www.ietf.org\/internet-drafts\/draft-ietf-manet-aodv-10.txt. North-Holland Amsterdam.   Perkins C. Royer E. and Das S. 2002. Ad hoc on demand distance vector (aodv) routing. In IETF Draft. http:\/\/www.ietf.org\/internet-drafts\/draft-ietf-manet-aodv-10.txt. North-Holland Amsterdam.","DOI":"10.17487\/rfc3561"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), T. Margaria and W. Yi, Eds. Lecture Notes in Computer Science","volume":"2031","author":"Pnueli A."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification, N. Halbwachs and D. Peled, Eds. Lecture Notes in Computer Science","volume":"1633","author":"Sa\u00efdi H."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science","volume":"2404","author":"Strichman O."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Thomas W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science Volume B: Formal Models and Sematics.   Thomas W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science Volume B: Formal Models and Sematics.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1297658.1297662","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1297658.1297662","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:14:03Z","timestamp":1750259643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1297658.1297662"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["10.1145\/1297658.1297662"],"URL":"https:\/\/doi.org\/10.1145\/1297658.1297662","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12]]},"assertion":[{"value":"2007-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}