{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:57Z","timestamp":1772164077596,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"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":["CCF 1115448"],"award-info":[{"award-number":["CCF 1115448"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["321174-VSSC"],"award-info":[{"award-number":["321174-VSSC"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["652\/11"],"award-info":[{"award-number":["652\/11"]}],"id":[{"id":"10.13039\/501100003977","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.2837640","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"217-231","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Decidability of inferring inductive invariants"],"prefix":"10.1145","author":[{"given":"Oded","family":"Padon","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[{"name":"University of Massachusetts at Amherst, USA"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Academic College of Tel Aviv Yaffo, Israel"}]},{"given":"Aleksandr","family":"Karbyshev","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"170","volume-title":"Logic in Computer Science, 1993. LICS\u201993., Proceedings of Eighth Annual IEEE Symposium on","author":"Abdulla P.","unstructured":"P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In Logic in Computer Science, 1993. LICS\u201993., Proceedings of Eighth Annual IEEE Symposium on, pages 160\u2013170. IEEE, 1993."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00105-5"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788796"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2843"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763580"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_33"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054113400078"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0111-7"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905411340008X"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604142"},{"key":"e_1_3_2_1_12_1","volume-title":"Model Theory. Studies in Logic and the Foundations of Mathematics","author":"Chang C.","year":"1990","unstructured":"C. Chang and H. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1990."},{"key":"e_1_3_2_1_13_1","unstructured":"ISBN 9780080880075."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926399"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03456-5_28"},{"key":"e_1_3_2_1_20_1","volume-title":"Invariant generation through strategy iteration in succinctly represented control flow graphs. Logical Methods in Computer Science, 8(3)","author":"Gawlitza T. M.","year":"2012","unstructured":"T. M. Gawlitza and D. Monniaux. Invariant generation through strategy iteration in succinctly represented control flow graphs. Logical Methods in Computer Science, 8(3), 2012."},{"key":"e_1_3_2_1_21_1","volume-title":"Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4)","author":"Ghilardi S.","year":"2010","unstructured":"S. Ghilardi and S. Ranise. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4), 2010.. URL http:\/\/dx.doi. org\/10.2168\/LMCS-6(4:10)2010."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_3_2_1_25_1","volume-title":"Graduate Texts in Computer Science","author":"Immerman N.","year":"1999","unstructured":"N. Immerman. Descriptive Complexity. Graduate Texts in Computer Science. Springer, 1999."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"e_1_3_2_1_27_1","volume-title":"CAV","author":"Karbyshev A.","year":"2015","unstructured":"A. Karbyshev, N. Bjorner, S. Itzhaky, N. Rinetzky, and S. Shoham. Property-directed inference of universal invariants or proving their absence. In CAV, 2015."},{"issue":"2","key":"e_1_3_2_1_28_1","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture","volume":"95","author":"Kruskal J.","year":"1960","unstructured":"J. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture. Transactions of the American Mathematical Society, 95(2), May 1960.","journal-title":"Transactions of the American Mathematical Society"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.10"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00646-1"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_1_34_1","first-page":"59","article-title":"On well-quasi-ordering finite trees","author":"Nash-Williams C.","year":"1963","unstructured":"C. Nash-Williams. On well-quasi-ordering finite trees. In Proc. Of the Cambridge Phil. Soc. 59, 1963.","journal-title":"Proc. Of the Cambridge Phil. Soc."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_21"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1881552.1881556"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15155-2_54"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.035"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.02.003"}],"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.2837640","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837640","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837640","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:28:33Z","timestamp":1763458113000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837640"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":40,"alternative-id":["10.1145\/2837614.2837640","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837640","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837640","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"}}]}}