{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:07Z","timestamp":1775873407451,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"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":[[2020,6,11]]},"DOI":"10.1145\/3385412.3386018","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"703-717","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["First-order quantified separators"],"prefix":"10.1145","author":[{"given":"Jason R.","family":"Koenig","sequence":"first","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[{"name":"University of Massachusetts at Amherst, USA"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"McMillan","author":"Albarghouthi Aws","year":"2013","unstructured":"Aws Albarghouthi and Kenneth L. McMillan. 2013. Beautiful Interpolants. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 313\u2013329."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"e_1_3_2_1_4_1","volume-title":"SAT-Based Model Checking without Unrolling","author":"Bradley Aaron R.","unstructured":"Aaron R. Bradley. 2011. SAT-Based Model Checking without Unrolling. In Verification, Model Checking, and Abstract Interpretation, Ranjit Jhala and David Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 70\u201387."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1164"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_12"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371073"},{"key":"e_1_3_2_1_11_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Feldman Yotam M. Y.","unstructured":"Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham. 2017. Bounded Quantifier Instantiation for Checking Inductive Invariants. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 76\u201395."},{"key":"e_1_3_2_1_12_1","volume-title":"Inferring Inductive Invariants from Phase Structures","author":"Feldman Yotam M. Y.","unstructured":"Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, and Mooly Sagiv. 2019. Inferring Inductive Invariants from Phase Structures. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 405\u2013425."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.43.1.163"},{"key":"e_1_3_2_1_14_1","volume-title":"ICE: A Robust Framework for Learning Invariants","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, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 69\u201387."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883627"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Neil Immerman. 1999. Descriptive Complexity. Springer.","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4478-3_5"},{"key":"e_1_3_2_1_18_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. The MIT Press."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2487050"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_2_1_22_1","volume-title":"18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science), Thomas Ball and Robert B. Jones (Eds.)","volume":"4144","author":"McMillan Kenneth L.","year":"2006","unstructured":"Kenneth L. McMillan. 2006. Lazy Abstraction with Interpolants. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science), Thomas Ball and Robert B. Jones (Eds.), Vol. 4144."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Springer 123\u2013136. 10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_3_2_1_28_1","volume-title":"Nori","author":"Sharma Rahul","year":"2013","unstructured":"Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori. 2013. Verification as Learning Geometric Concepts. In Static Analysis, Francesco Logozzo and Manuel F\u00e4hndrich (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 388\u2013411."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535853"},{"key":"e_1_3_2_1_30_1","unstructured":"Marcelo Taube Giuliano Losa Kenneth L. McMillan Oded Padon Mooly Sagiv Sharon Shoham James R. Wilcox and Doug Woos. 2018."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","unstructured":"V. Vapnik and A. Chervonenkis. 1971. On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities. Theory of Probability & Its Applications 16 2 (1971) 264\u2013280. 10.1137\/1116025","DOI":"10.1137\/1116025"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386018","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3386018","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:49Z","timestamp":1750199929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386018"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":32,"alternative-id":["10.1145\/3385412.3386018","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3386018","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}