{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:21:57Z","timestamp":1750220517714,"version":"3.41.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"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":[[2021,1,4]]},"abstract":"<jats:p>We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, which permits applying theoretical results from exact concept learning to answer open problems in invariant inference theory. The condition requires the invariant's boundary---the states whose Hamming distance from the invariant is one---to be backwards reachable from the bad states in a small number of steps. Using this condition, we obtain the first polynomial complexity result for an interpolation-based invariant inference algorithm, efficiently inferring monotone DNF invariants with access to a SAT solver as an oracle. We further harness Bshouty's seminal result in concept learning to efficiently infer invariants of a larger syntactic class of invariants beyond monotone DNF. Lastly, we consider the robustness of inference under program transformations. We show that some simple transformations preserve the fence condition, and that it is sensitive to more complex transformations.<\/jats:p>","DOI":"10.1145\/3434296","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Learning the boundary of inductive invariants"],"prefix":"10.1145","volume":"5","author":[{"given":"Yotam M. Y.","family":"Feldman","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"James R.","family":"Wilcox","sequence":"additional","affiliation":[{"name":"Certora, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2465220"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00996269"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"e_1_2_1_4_1","first-page":"1","article-title":"Syntax-Guided Synthesis","author":"Alur Rajeev","year":"2015","unstructured":"Rajeev Alur , Rastislav Bod\u00edk , Eric Dallal , Dana Fisman , Pranav Garg , Garvit Juniwal , Hadas Kress-Gazit , P. Madhusudan , Milo M. K. Martin , Mukund Raghothaman , Shambwaditya Saha , Sanjit A. Seshia , Rishabh Singh , Armando Solar-Lezama , Emina Torlak , and Abhishek Udupa . 2015 . Syntax-Guided Synthesis . In Dependable Software Systems Engineering. 1 - 25 . Rajeev Alur, Rastislav Bod\u00edk, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2015. Syntax-Guided Synthesis. In Dependable Software Systems Engineering. 1-25.","journal-title":"Dependable Software Systems Engineering."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Dana Angluin. 1987. Queries and Concept Learning. Machine Learning 2 4 ( 1987 ) 319-342.  Dana Angluin. 1987. Queries and Concept Learning. Machine Learning 2 4 ( 1987 ) 319-342.","DOI":"10.1007\/BF00116828"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138061"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_9_1","first-page":"35","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 - 41 . 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-41. https:\/\/easychair.org\/publications\/paper\/XtN"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1164"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01262930"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.04.034"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(78)90168-1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_44"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_12"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838559"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_2_1_20_1","volume-title":"Hammer","author":"Crama Yves","year":"2011","unstructured":"Yves Crama and Peter L . Hammer . 2011 . Boolean Functions-Theory, Algorithms , and Applications. Encyclopedia of mathematics and its applications, Vol. 142 . Cambridge University Press . http:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/ item6222210\/?site_locale=en_GB Yves Crama and Peter L. Hammer. 2011. Boolean Functions-Theory, Algorithms, and Applications. Encyclopedia of mathematics and its applications, Vol. 142. Cambridge University Press. http:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/ item6222210\/?site_locale=en_GB"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290358"},{"key":"e_1_2_1_22_1","first-page":"443","volume-title":"Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013","author":"Dillig Isil","year":"2013","unstructured":"Isil Dillig , Thomas Dillig , Boyang Li , and Kenneth L . McMillan. 2013. Inductive invariant generation via abductive inference . In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013 , Indianapolis, IN, USA , October 26-31, 2013 . 443 - 456 . Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. 2013. Inductive invariant generation via abductive inference. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013. 443-456."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_12"},{"key":"e_1_2_1_24_1","volume-title":"International Conference on Formal Methods in Computer-Aided Design, FMCAD '11","author":"E\u00e9n Niklas","year":"2011","unstructured":"Niklas E\u00e9n , Alan Mishchenko , and Robert K. Brayton . 2011. Eficient implementation of property directed reachability . In International Conference on Formal Methods in Computer-Aided Design, FMCAD '11 , Austin, TX, USA, October 30- November 02, 2011 . 125-134. http:\/\/dl.acm.org\/citation.cfm?id= 2157675 Niklas E\u00e9n, Alan Mishchenko, and Robert K. Brayton. 2011. Eficient implementation of property directed reachability. In International Conference on Formal Methods in Computer-Aided Design, FMCAD '11, Austin, TX, USA, October 30-November 02, 2011. 125-134. http:\/\/dl.acm.org\/citation.cfm?id= 2157675"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_14"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371073"},{"key":"e_1_2_1_27_1","volume-title":"Wilcox","author":"Feldman Yotam M. Y.","year":"2021","unstructured":"Yotam M. Y. Feldman , Mooly Sagiv , Sharon Shoham , and James R . Wilcox . 2021 . Learning the Boundary of Inductive Invariants. CoRR abs\/ 2008.09909 ( 2021 ). https:\/\/arxiv.org\/abs\/ 2008.09909 Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox. 2021. Learning the Boundary of Inductive Invariants. CoRR abs\/ 2008.09909 ( 2021 ). https:\/\/arxiv.org\/abs\/ 2008.09909"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_23"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_32_1","volume-title":"ICE: A robust framework for learning invariants. In Computer Aided Verification","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 . Springer , 69-87. Pranav Garg, Christof L\u00f6ding, P Madhusudan, and Daniel Neider. 2014. ICE: A robust framework for learning invariants. In Computer Aided Verification. Springer, 69-87."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000078"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_6"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.13"},{"volume-title":"22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 214-229","author":"Shuvendu","key":"e_1_2_1_44_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-229 . 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-229."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594326"},{"key":"e_1_2_1_47_1","volume-title":"15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1-13","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-13 . 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-13."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157661"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_14"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_22"},{"volume-title":"Analysis of Boolean Functions","author":"O'Donnell Ryan","key":"e_1_2_1_53_1","unstructured":"Ryan O'Donnell . 2014. Analysis of Boolean Functions . Cambridge University Press . http:\/\/www.cambridge.org\/de\/ academic\/subjects\/computer-science\/ algorithmics-complexity-computer-algebra-and-computational-g\/analysisboolean-functions Ryan O'Donnell. 2014. Analysis of Boolean Functions. Cambridge University Press. http:\/\/www.cambridge.org\/de\/ academic\/subjects\/computer-science\/ algorithmics-complexity-computer-algebra-and-computational-g\/analysisboolean-functions"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022643204877"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0248-5"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_57"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"volume-title":"Static Analysis-20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388-411","author":"Sharma Rahul","key":"e_1_2_1_59_1","unstructured":"Rahul Sharma , Saurabh Gupta , Bharath Hariharan , Alex Aiken , and Aditya V. Nori . 2013a. Verification as Learning Geometric Concepts . In Static Analysis-20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388-411 . Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori. 2013a. Verification as Learning Geometric Concepts. In Static Analysis-20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388-411."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1137\/050632026"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1968.1972"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_43"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0224-5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434296","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434296","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434296"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":64,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434296"],"URL":"https:\/\/doi.org\/10.1145\/3434296","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}