{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:17Z","timestamp":1751662877548,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>Inferring inductive invariants is one of the main challenges of formal verification. The theory of abstract interpretation provides a rich framework to devise invariant inference algorithms. One of the latest breakthroughs in invariant inference is property-directed reachability (PDR), but the research community views PDR and abstract interpretation as mostly unrelated techniques.<\/jats:p>\n          <jats:p>This paper shows that, surprisingly, propositional PDR can be formulated as an abstract interpretation algorithm in a logical domain. More precisely, we define a version of PDR, called \u039b-PDR, in which all generalizations of counterexamples are used to strengthen a frame. In this way, there is no need to refine frames after their creation, because all the possible supporting facts are included in advance. We analyze this algorithm using notions from Bshouty\u2019s monotone theory, originally developed in the context of exact learning. We show that there is an inherent overapproximation between the algorithm\u2019s frames that is related to the monotone theory. We then define a new abstract domain in which the best abstract transformer performs this overapproximation, and show that it captures the invariant inference process, i.e., \u039b-PDR corresponds to Kleene iterations with the best transformer in this abstract domain. We provide some sufficient conditions for when this process converges in a small number of iterations, with sometimes an exponential gap from the number of iterations required for naive exact forward reachability. These results provide a firm theoretical foundation for the benefits of how PDR tackles forward reachability.<\/jats:p>","DOI":"10.1145\/3498676","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Property-directed reachability as abstract interpretation in the monotone theory"],"prefix":"10.1145","volume":"6","author":[{"given":"Yotam M. Y.","family":"Feldman","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James R.","family":"Wilcox","sequence":"additional","affiliation":[{"name":"Certora, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9450-z"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006887"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_12"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_2_7_1","volume-title":"LPAR","author":"Bj\u00f8rner Nikolaj","year":"2013","unstructured":"Nikolaj Bj\u00f8rner , Arie Gurfinkel , Konstantin Korovin , and Ori Lahav . 2013. Instantiations , Zippers and EPR Interpolation . In LPAR 2013 , 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings. 35\u201341. https:\/\/easychair.org\/publications\/paper\/XtN Nikolaj Bj\u00f8rner, Arie Gurfinkel, Konstantin Korovin, and Ori Lahav. 2013. Instantiations, Zippers and EPR Interpolation. In LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings. 35\u201341. https:\/\/easychair.org\/publications\/paper\/XtN"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1164"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_44"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_12"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"volume-title":"Systematic Design of Program Analysis Frameworks. In Symp. on Princ. of Prog. Lang.. ACM Press","author":"Cousot P.","key":"e_1_2_2_14_1","unstructured":"P. Cousot and R. Cousot . 1979 . Systematic Design of Program Analysis Frameworks. In Symp. on Princ. of Prog. Lang.. ACM Press , New York, NY. 269\u2013282. P. Cousot and R. Cousot. 1979. Systematic Design of Program Analysis Frameworks. In Symp. on Princ. of Prog. Lang.. ACM Press, New York, NY. 269\u2013282."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_2_2_17_1","volume-title":"International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911","author":"E\u00e9n Niklas","year":"2011","unstructured":"Niklas E\u00e9n , Alan Mishchenko , and Robert K. Brayton . 2011. Efficient implementation of property directed reachability . In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911 , Austin, TX, USA, October 30 - November 02, 2011 . 125\u2013134. http:\/\/dl.acm.org\/citation.cfm?id=2157675 Niklas E\u00e9n, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA, October 30 - November 02, 2011. 125\u2013134. http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"P. Ezudheen Daniel Neider Deepak D\u2019Souza Pranav Garg and P. Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts. PACMPL 2 OOPSLA (2018) 131:1\u2013131:25.  P. Ezudheen Daniel Neider Deepak D\u2019Souza Pranav Garg and P. Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts. PACMPL 2 OOPSLA (2018) 131:1\u2013131:25.","DOI":"10.1145\/3276501"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_12"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371073"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434296"},{"key":"e_1_2_2_22_1","volume-title":"Wilcox","author":"Feldman Yotam M. Y.","year":"2022","unstructured":"Yotam M. Y. Feldman , Mooly Sagiv , Sharon Shoham , and James R . Wilcox . 2022 . Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. CoRR , arxiv:2111.00324 Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox. 2022. Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. CoRR, arxiv:2111.00324"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_2_25_1","volume-title":"ICE: A robust framework for learning invariants. In Computer Aided Verification. 69\u201387.","author":"Garg Pranav","year":"2014","unstructured":"Pranav Garg , Christof L\u00f6ding , P Madhusudan , and Daniel Neider . 2014 . ICE: A robust framework for learning invariants. In Computer Aided Verification. 69\u201387. Pranav Garg, Christof L\u00f6ding, P Madhusudan, and Daniel Neider. 2014. ICE: A robust framework for learning invariants. In Computer Aided Verification. 69\u201387."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"e_1_2_2_29_1","volume-title":"FMCAD 2015","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel and Alexander Ivrii . 2015 . Pushing to the Top. In Formal Methods in Computer-Aided Design , FMCAD 2015 , Austin, Texas, USA , September 27-30, 2015.. 65\u201372. Arie Gurfinkel and Alexander Ivrii. 2015. Pushing to the Top. In Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015.. 65\u201372."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/12130.12132"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.10.015"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0294-5"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000078"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_10"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009860"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36384-X_24"},{"volume-title":"22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 214\u2013229","author":"Shuvendu","key":"e_1_2_2_41_1","unstructured":"Shuvendu K. Lahiri and Shaz Qadeer. 2009. Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. In Automated Deduction - CADE-22 , 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 214\u2013229 . Shuvendu K. Lahiri and Shaz Qadeer. 2009. Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 214\u2013229."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113738"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_44_1","volume-title":"15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1\u201313","author":"McMillan Kenneth L.","year":"2003","unstructured":"Kenneth L. McMillan . 2003 . Interpolation and SAT-Based Model Checking. In Computer Aided Verification , 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1\u201313 . Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1\u201313."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09570-z"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837640"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_2_2_48_1","volume-title":"Two theorems about truth-functions. Bolet\u00edn de la Sociedad Matem\u00e1tica Mexicana, 10, 1\u20132","author":"Quine WV","year":"1954","unstructured":"WV Quine . 1954. Two theorems about truth-functions. Bolet\u00edn de la Sociedad Matem\u00e1tica Mexicana, 10, 1\u20132 ( 1954 ), 64\u201370. WV Quine. 1954. Two theorems about truth-functions. Bolet\u00edn de la Sociedad Matem\u00e1tica Mexicana, 10, 1\u20132 (1954), 64\u201370."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_5"},{"key":"e_1_2_2_50_1","volume-title":"Computing Upper Bounds on Lengths of Transition Sequences. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence","author":"Rintanen Jussi","year":"2013","unstructured":"Jussi Rintanen and Charles Orgill Gretton . 2013 . Computing Upper Bounds on Lengths of Transition Sequences. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence , Beijing, China , August 3-9, 2013, Francesca Rossi (Ed.). IJCAI\/AAAI, 2365\u20132372. http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6992 Jussi Rintanen and Charles Orgill Gretton. 2013. Computing Upper Bounds on Lengths of Transition Sequences. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, Francesca Rossi (Ed.). IJCAI\/AAAI, 2365\u20132372. http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6992"},{"volume-title":"Introduction to Static Analysis: An Abstract Interpretation Perspective","author":"Rival Xavier","key":"e_1_2_2_51_1","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis: An Abstract Interpretation Perspective . MIT Press . Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press."},{"key":"e_1_2_2_52_1","volume-title":"Completeness in the polynomial-time hierarchy: A compendium. SIGACT news, 33, 3","author":"Schaefer Marcus","year":"2002","unstructured":"Marcus Schaefer and Christopher Umans . 2002. Completeness in the polynomial-time hierarchy: A compendium. SIGACT news, 33, 3 ( 2002 ), 32\u201349. Marcus Schaefer and Christopher Umans. 2002. Completeness in the polynomial-time hierarchy: A compendium. SIGACT news, 33, 3 (2002), 32\u201349."},{"key":"e_1_2_2_53_1","volume-title":"MBMV 2017","author":"Seufert Tobias","year":"2017","unstructured":"Tobias Seufert and Christoph Scholl . 2017 . Sequential Verification Using Reverse PDR. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen , MBMV 2017 , Bremen, Germany , February 8-9, 2017, Daniel Gro\u00df e and Rolf Drechsler (Eds.). Shaker Verlag, 79\u201390. Tobias Seufert and Christoph Scholl. 2017. Sequential Verification Using Reverse PDR. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV 2017, Bremen, Germany, February 8-9, 2017, Daniel Gro\u00df e and Rolf Drechsler (Eds.). Shaker Verlag, 79\u201390."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0248-5"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"volume-title":"SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388\u2013411","author":"Sharma Rahul","key":"e_1_2_2_56_1","unstructured":"Rahul Sharma , Saurabh Gupta , Bharath Hariharan , Alex Aiken , and Aditya V. Nori . 2013. Verification as Learning Geometric Concepts. In Static Analysis - 20th International Symposium , SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388\u2013411 . Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori. 2013. Verification as Learning Geometric Concepts. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388\u2013411."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2001.1775"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498676","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498676","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498676"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498676"],"URL":"https:\/\/doi.org\/10.1145\/3498676","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}