{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:10Z","timestamp":1775873530567,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"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":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192416","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"707-721","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":48,"title":["A data-driven CHC solver"],"prefix":"10.1145","author":[{"given":"He","family":"Zhu","sequence":"first","affiliation":[{"name":"Galois, USA"}]},{"given":"Stephen","family":"Magill","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_20"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961189.1961199"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110270"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007662407062"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_2_12_1","first-page":"307","volume-title":"CAV 2015, San Francisco, CA, USA, Proceedings, Part I. Springer-Verlag New York, Inc.","author":"Gehr Timon","unstructured":"Timon Gehr , Dimitar Dimitrov , and Martin T. Vechev . 2015. Learning Commutativity Specifications. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, Proceedings, Part I. Springer-Verlag New York, Inc. , New York, NY, USA , 307 - 323 . Timon Gehr, Dimitar Dimitrov, and Martin T. Vechev. 2015. Learning Commutativity Specifications. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, Proceedings, Part I. Springer-Verlag New York, Inc., New York, NY, USA, 307-323."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_3_2_2_15_1","first-page":"343","volume-title":"CAV 2015, San Francisco, CA, USA, Proceedings, Part I. Springer-Verlag New York, Inc.","author":"Gurfinkel Arie","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge A. Navas . 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, Proceedings, Part I. Springer-Verlag New York, Inc. , New York, NY, USA , 343 - 361 . Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, Proceedings, Part I. Springer-Verlag New York, Inc., New York, NY, USA, 343-361."},{"key":"e_1_3_2_2_16_1","first-page":"471","volume-title":"Nested Interpolants. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '10)","author":"Heizmann Matthias","year":"2010","unstructured":"Matthias Heizmann , Jochen Hoenicke , and Andreas Podelski . 2010 . Nested Interpolants. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '10) . ACM, New York, NY, USA , 471 - 482 . Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2010. Nested Interpolants. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '10). ACM, New York, NY, USA, 471-482."},{"key":"e_1_3_2_2_17_1","first-page":"157","volume-title":"Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT'12)","author":"Nikolaj Bjurner Hoder","year":"2012","unstructured":"Kry?tof Hoder and Nikolaj Bjurner . 2012 . Generalized Property Directed Reachability . In Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT'12) . Springer-Verlag, Berlin, Heidelberg , 157 - 171 . Kry?tof Hoder and Nikolaj Bjurner. 2012. Generalized Property Directed Reachability. In Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT'12). Springer-Verlag, Berlin, Heidelberg, 157-171."},{"key":"e_1_3_2_2_18_1","first-page":"352","volume-title":"CAV 2016, Toronto, ON, Canada, Proceedings, Part I. Springer-Verlag New York, Inc.","author":"Kahsai Temesghen","year":"2016","unstructured":"Temesghen Kahsai , Philipp Rummer , Huascar Sanchez , and Martin Schaf . 2016 . JayHorn: A Framework for Verifying Java programs. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, Proceedings, Part I. Springer-Verlag New York, Inc. , New York, NY, USA , 352 - 358 . Temesghen Kahsai, Philipp Rummer, Huascar Sanchez, and Martin Schaf. 2016. JayHorn: A Framework for Verifying Java programs. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, Proceedings, Part I. Springer-Verlag New York, Inc., New York, NY, USA, 352-358."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_2_20_1","unstructured":"Siddharth Krishna Christian Puhrsch and Thomas Wies. 2015. Learning Invariants using Decision Trees. http:\/\/cs.nyu.edu\/~siddharth\/invariants_dt.pdf.  Siddharth Krishna Christian Puhrsch and Thomas Wies. 2015. Learning Invariants using Decision Trees. http:\/\/cs.nyu.edu\/~siddharth\/invariants_dt.pdf."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155660"},{"key":"e_1_3_2_2_22_1","first-page":"1","volume-title":"15th International Conference, CAV 2003, Boulder, CO, USA, Proceedings. Springer-Verlag","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, Proceedings. Springer-Verlag , Berlin, Heidelberg , 1 - 13 . Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, Proceedings. Springer-Verlag, Berlin, Heidelberg, 1-13."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_16"},{"key":"e_1_3_2_2_25_1","unstructured":"K. L. McMillan and A. Rybalchenko. 2013. Computing Relational Fixed Points Using Interpolation. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/MSR-TR-2013-6.pdf.  K. L. McMillan and A. Rybalchenko. 2013. Computing Relational Fixed Points Using Interpolation. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/MSR-TR-2013-6.pdf."},{"key":"e_1_3_2_2_26_1","unstructured":"LinearArbitrary. 2018. https:\/\/github.com\/GaloisInc\/LinearArbitrary-SeaHorn\/.  LinearArbitrary. 2018. https:\/\/github.com\/GaloisInc\/LinearArbitrary-SeaHorn\/."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568275"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_2_30_1","volume-title":"Advances in Kernel Methods","author":"Platt John C.","unstructured":"John C. Platt . 1999. Advances in Kernel Methods . MIT Press , Cambridge, MA, USA , Chapter Fast Training of Support Vector Machines Using Sequential Minimal Optimization, 185-208. John C. Platt. 1999. Advances in Kernel Methods. MIT Press, Cambridge, MA, USA, Chapter Fast Training of Support Vector Machines Using Sequential Minimal Optimization, 185-208."},{"key":"e_1_3_2_2_31_1","volume-title":"Programs for Machine Learning","author":"Quinlan J. Ross","unstructured":"J. Ross Quinlan . 1993. C4.5 : Programs for Machine Learning . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA. J. Ross Quinlan. 1993. C4.5: Programs for Machine Learning. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958101"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390666"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/584091.584093"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_3_2_2_36_1","first-page":"574","volume-title":"Proceedings of the 22Nd European Conference on Programming Languages and Systems (ESOP'13)","author":"Sharma Rahul","unstructured":"Rahul Sharma , Saurabh Gupta , Bharath Hariharan , Alex Aiken , Percy Liang , and Aditya V. Nori . 2013. A Data Driven Approach for Algebraic Loop Invariants . In Proceedings of the 22Nd European Conference on Programming Languages and Systems (ESOP'13) . Springer-Verlag, Berlin, Heidelberg , 574 - 592 . Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya V. Nori. 2013. A Data Driven Approach for Algebraic Loop Invariants. In Proceedings of the 22Nd European Conference on Programming Languages and Systems (ESOP'13). Springer-Verlag, Berlin, Heidelberg, 574-592."},{"key":"e_1_3_2_2_37_1","first-page":"388","volume-title":"SAS 2013, Seattle, WA, USA, Proceedings. Springer-Verlag","author":"Sharma Rahul","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, Proceedings. Springer-Verlag , Berlin, Heidelberg , 388 - 411 . 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, Proceedings. Springer-Verlag, Berlin, Heidelberg, 388-411."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_3_2_2_39_1","unstructured":"SV-COMP. 2017. http:\/\/sv-comp.sosy-lab.org\/2017\/.  SV-COMP. 2017. http:\/\/sv-comp.sosy-lab.org\/2017\/."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908125"}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192416","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192416","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192416"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":40,"alternative-id":["10.1145\/3192366.3192416","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192416","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192416","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}