{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:11Z","timestamp":1775873531413,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T00:00:00Z","timestamp":1484092800000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1138994"],"award-info":[{"award-number":["1138994"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006502","name":"Defense Sciences Office, DARPA","doi-asserted-by":"publisher","award":["FA8750-13-2-0008"],"award-info":[{"award-number":["FA8750-13-2-0008"]}],"id":[{"id":"10.13039\/100006502","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837664","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"499-512","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":103,"title":["Learning invariants using decision trees and implication counterexamples"],"prefix":"10.1145","author":[{"given":"Pranav","family":"Garg","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Dan","family":"Roth","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Competition on Software Verification (SV-COMP) benchmarks. https:\/\/svn.sosy-lab.org\/software\/ sv-benchmarks\/tags\/svcomp14\/loops\/."},{"key":"e_1_3_2_2_2_1","volume-title":"Artificial Intelligence, (0):\u2013","author":"Learning","year":"2015","unstructured":"Learning bayesian network parameters under equivalence constraints. Artificial Intelligence, (0):\u2013, 2015."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958099"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_52"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022821128753"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1296180"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384625"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032321"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/279943.279962"},{"key":"e_1_3_2_2_14_1","unstructured":"ISBN 1-58113-057-0."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_10"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765903"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_2_19_1","series-title":"LNCS","first-page":"432","volume-title":"CAV","author":"Col\u00f3n M.","year":"2003","unstructured":"M. Col\u00f3n, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In CAV 2003, volume 2725 of LNCS, pages 420\u2013432. Springer, 2003."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022627411411"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337240"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_2_2_25_1","series-title":"LNCS","first-page":"829","volume-title":"CAV","author":"Garg P.","year":"2013","unstructured":"P. Garg, C. L\u00f6ding, P. Madhusudan, and D. Neider. Learning universally quantified invariants of linear data structures. In CAV 2013, volume 8044 of LNCS, pages 813\u2013829. Springer, 2013."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_10"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_3_2_2_31_1","unstructured":"F. Ivancic and S. Sankaranarayanan. NECLA Benchmarks. http: \/\/www.nec-labs.com\/research\/system\/systems_ SAV-website\/small_static_bench-v1.1.tar.gz."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/200548"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1947873.1947904"},{"key":"e_1_3_2_2_36_1","volume-title":"Learning invariants using decision trees. CoRR, abs\/1501.04725","author":"Krishna S.","year":"2015","unstructured":"S. Krishna, C. Puhrsch, and T. Wies. Learning invariants using decision trees. CoRR, abs\/1501.04725, 2015."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022869011914"},{"key":"e_1_3_2_2_38_1","series-title":"LNCS","first-page":"13","volume-title":"CAV","author":"McMillan K. L.","unstructured":"K. L. McMillan. Interpolation and SAT-Based model checking. In CAV, volume 2725 of LNCS, pages 1\u201313. Springer, 2003."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/541177"},{"key":"e_1_3_2_2_41_1","unstructured":"D. Neider. Applications of Automata Learning in Versification and Synthesis. PhD thesis RWTH Aachen University April 2014."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337304"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022643204877"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/152181"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1037\/h0042519"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1948.tb01338.x"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_3_2_2_53_1","series-title":"LNCS","first-page":"411","volume-title":"SAS","author":"Sharma R.","unstructured":"R. Sharma, S. Gupta, B. Hariharan, A. Aiken, and A. V. Nori. Verification as learning geometric concepts. In SAS, volume 7935 of LNCS, pages 388\u2013411. Springer, 2013."},{"key":"e_1_3_2_2_54_1","unstructured":"A. Solar Lezama. Program Synthesis By Sketching. PhD thesis EECS Department University of California Berkeley Dec 2008."},{"key":"e_1_3_2_2_55_1","unstructured":"A. Thakur A. Lal J. Lim and T. Reps. Posthat and all that: Attaining most-precise inductive invariants. Technical Report TR1790 University of Wisconsin Madison WI Apr 2013."},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0026-x"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837664","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837664","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837664","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:28:10Z","timestamp":1763458090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837664"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":56,"alternative-id":["10.1145\/2837614.2837664","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837664","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837664","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}