{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:43Z","timestamp":1762459663069,"version":"3.41.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,10,24]]},"abstract":"<jats:p>We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from nonlinear Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using nonlinear Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.<\/jats:p>","DOI":"10.1145\/3276501","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":48,"title":["Horn-ICE learning for synthesizing invariants and contracts"],"prefix":"10.1145","volume":"2","author":[{"given":"P.","family":"Ezudheen","sequence":"first","affiliation":[{"name":"IISc Bangalore, India"}]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Deepak","family":"D'Souza","sequence":"additional","affiliation":[{"name":"IISc Bangalore, India"}]},{"given":"Pranav","family":"Garg","sequence":"additional","affiliation":[{"name":"Amazon, India"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_2_2_4_1","volume-title":"Solving Existentially Quantified Horn Clauses. In CAV 2013 (LNCS). Springer, 869\u2013882","author":"Beyene Tewodros A.","year":"2013","unstructured":"Tewodros A. Beyene , Corneliu Popeea , and Andrey Rybalchenko . 2013 . Solving Existentially Quantified Horn Clauses. In CAV 2013 (LNCS). Springer, 869\u2013882 . Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In CAV 2013 (LNCS). Springer, 869\u2013882."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"e_1_2_2_6_1","volume-title":"On Solving Universally Quantified Horn Clauses. In SAS","author":"Bj\u00f8rner Nikolaj","year":"2013","unstructured":"Nikolaj Bj\u00f8rner , Kenneth L. McMillan , and Andrey Rybalchenko . 2013 . On Solving Universally Quantified Horn Clauses. In SAS 2013. 105\u2013125. Nikolaj Bj\u00f8rner, Kenneth L. McMillan, and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS 2013. 105\u2013125."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_2_2_8_1","volume-title":"Learning Shape Analysis. In SAS","author":"Brockschmidt Marc","year":"2017","unstructured":"Marc Brockschmidt , Yuxin Chen , Pushmeet Kohli , Siddharth Krishna , and Daniel Tarlow . 2017 . Learning Shape Analysis. In SAS 2017. 66\u201387. Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, and Daniel Tarlow. 2017. Learning Shape Analysis. In SAS 2017. 66\u201387."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_20"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509517"},{"key":"e_1_2_2_11_1","volume-title":"Linear Invariant Generation Using Non-linear Constraint Solving. In CAV 2003 (LNCS)","volume":"2725","author":"Col\u00f3n Michael","year":"2003","unstructured":"Michael Col\u00f3n , Sriram Sankaranarayanan , and Henny Sipma . 2003 . Linear Invariant Generation Using Non-linear Constraint Solving. In CAV 2003 (LNCS) , Vol. 2725 . Springer, 420\u2013432. Michael Col\u00f3n, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In CAV 2003 (LNCS), Vol. 2725. Springer, 420\u2013432."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337240"},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Grigory Fedyukovich Samuel J Kaufman and Rastislav Bodik. 2017. Sampling Invariants from Frequency Distributions. (2017).  Grigory Fedyukovich Samuel J Kaufman and Rastislav Bodik. 2017. Sampling Invariants from Frequency Distributions. (2017).","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_2_2_19_1","volume-title":"Learning Universally Quantified Invariants of Linear Data Structures. In CAV 2013 (LNCS)","volume":"8044","author":"Garg Pranav","year":"2013","unstructured":"Pranav Garg , Christof L\u00f6ding , P. Madhusudan , and Daniel Neider . 2013 . Learning Universally Quantified Invariants of Linear Data Structures. In CAV 2013 (LNCS) , Vol. 8044 . Springer, 813\u2013829. Pranav Garg, Christof L\u00f6ding, P. Madhusudan, and Daniel Neider. 2013. Learning Universally Quantified Invariants of Linear Data Structures. In CAV 2013 (LNCS), Vol. 8044. Springer, 813\u2013829."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_2_2_25_1","volume-title":"The SeaHorn Verification Framework. In CAV 2015 (LNCS)","volume":"9206","author":"Gurfinkel Arie","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge A. Navas . 2015 . The SeaHorn Verification Framework. In CAV 2015 (LNCS) , Vol. 9206 . Springer, 343\u2013361. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV 2015 (LNCS), Vol. 9206. Springer, 343\u2013361."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_53"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_40"},{"key":"e_1_2_2_31_1","volume-title":"Interpolation and SAT-Based Model Checking. In CAV 2003 (LNCS)","volume":"2725","author":"McMillan Kenneth L.","year":"2003","unstructured":"Kenneth L. McMillan . 2003 . Interpolation and SAT-Based Model Checking. In CAV 2003 (LNCS) , Vol. 2725 . Springer, 1\u201313. Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In CAV 2003 (LNCS), Vol. 2725. Springer, 1\u201313."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"e_1_2_2_34_1","volume-title":"Invariant Synthesis for Incomplete Verification Engines. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 232\u2013250","author":"Neider Daniel","year":"2018","unstructured":"Daniel Neider , Pranav Garg , P Madhusudan , Shambwaditya Saha , and Daejun Park . 2018 . Invariant Synthesis for Incomplete Verification Engines. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 232\u2013250 . Daniel Neider, Pranav Garg, P Madhusudan, Shambwaditya Saha, and Daejun Park. 2018. Invariant Synthesis for Incomplete Verification Engines. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 232\u2013250."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337304"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970305"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022643204877"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_2_2_42_1","volume-title":"SAS 2013 (LNCS)","volume":"7935","author":"Sharma Rahul","unstructured":"Rahul Sharma , Saurabh Gupta , Bharath Hariharan , Alex Aiken , and Aditya V. Nori . 2013a. Verification as Learning Geometric Concepts . In SAS 2013 (LNCS) , Vol. 7935 . 388\u2013411. Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori. 2013a. Verification as Learning Geometric Concepts. In SAS 2013 (LNCS), Vol. 7935. 388\u2013411."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_28"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784766"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908125"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276501","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276501","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:39Z","timestamp":1750273419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276501"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":48,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276501"],"URL":"https:\/\/doi.org\/10.1145\/3276501","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}