{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T22:35:20Z","timestamp":1784932520054,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,21]],"date-time":"2022-05-21T00:00:00Z","timestamp":1653091200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2018YFB1308601"],"award-info":[{"award-number":["2018YFB1308601"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62072267, 62021002"],"award-info":[{"award-number":["62072267, 62021002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,21]]},"DOI":"10.1145\/3510003.3510220","type":"proceedings-article","created":{"date-parts":[[2022,7,5]],"date-time":"2022-07-05T22:42:59Z","timestamp":1657060979000},"page":"499-510","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Data-driven loop bound learning for termination analysis"],"prefix":"10.1145","author":[{"given":"Rongchen","family":"Xu","sequence":"first","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jianhui","family":"Chen","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa.","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. IEEE."},{"key":"e_1_3_2_1_2_1","volume-title":"OPTICS: Ordering points to identify the clustering structure. ACM Sigmod record 28, 2","author":"Ankerst Mihael","year":"1999","unstructured":"Mihael Ankerst, Markus M Breunig, Hans-Peter Kriegel, and J\u00f6rg Sander. 1999. OPTICS: Ordering points to identify the clustering structure. ACM Sigmod record 28, 2 (1999), 49--60."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429078"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund M Clarke Ofer Strichman and Yunshan Zhu. 2003. Bounded model checking. (2003).","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_1_5_1","volume-title":"Convex optimization","author":"Boyd Stephen","unstructured":"Stephen Boyd, Stephen P Boyd, and Lieven Vandenberghe. 2004. Convex optimization. Cambridge university press."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_37"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019225027893"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192405"},{"key":"e_1_3_2_1_10_1","volume-title":"Bounded model checking using satisfiability solving. Formal methods in system design 19, 1","author":"Clarke Edmund","year":"2001","unstructured":"Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. 2001. Bounded model checking using satisfiability solving. Formal methods in system design 19, 1 (2001), 7--34."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133255.1134029"},{"key":"e_1_3_2_1_12_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 47--61","author":"Zuleger Florian","year":"2013","unstructured":"Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. lexicographic termination proving. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 47--61."},{"key":"e_1_3_2_1_13_1","unstructured":"Martin Ester Hans-Peter Kriegel J\u00f6rg Sander Xiaowei Xu et al. 1996. A density-based algorithm for discovering clusters in large spatial databases with noise.. In kdd Vol. 96. 226--231."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_7"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837664"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_19"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_53"},{"key":"e_1_3_2_1_21_1","unstructured":"Dieter Kraft et al. 1988. A software package for sequential quadratic programming. (1988)."},{"key":"e_1_3_2_1_22_1","volume-title":"Learning invariants using decision trees. arXiv preprint arXiv:1501.04725","author":"Krishna Siddharth","year":"2015","unstructured":"Siddharth Krishna, Christian Puhrsch, and Thomas Wies. 2015. Learning invariants using decision trees. arXiv preprint arXiv:1501.04725 (2015)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_4"},{"key":"e_1_3_2_1_25_1","volume-title":"Proving termination of imperative programs using Max-SMT. In 2013 Formal Methods in Computer-Aided Design","author":"Larraz Daniel","unstructured":"Daniel Larraz, Albert Oliveras, Enric Rodr\u00edguez-Carbonell, and Albert Rubio. 2013. Proving termination of imperative programs using Max-SMT. In 2013 Formal Methods in Computer-Aided Design. IEEE, 218--225."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428257"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737993"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_12"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115689"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the fifth Berkeley symposium on mathematical statistics and probability","volume":"1","author":"James","unstructured":"James MacQueen et al. 1967. Some methods for classification and analysis of multivariate observations. In Proceedings of the fifth Berkeley symposium on mathematical statistics and probability, Vol. 1. Oakland, CA, USA, 281--297."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491413"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908099"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_2_1_34_1","volume-title":"International Symposium on Practical Aspects of Declarative Languages. Springer, 245--259","author":"Podelski Andreas","year":"2007","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2007. ARMC: the logical choice for software model checking with abstraction refinement. In International Symposium on Practical Aspects of Declarative Languages. Springer, 245--259."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_2"},{"key":"e_1_3_2_1_36_1","volume-title":"Advances in optimization and numerical analysis","author":"Powell Michael JD","unstructured":"Michael JD Powell. 1994. A direct search optimization method that models the objective and constraint functions by linear interpolation. In Advances in optimization and numerical analysis. Springer, 51--67."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_3_2_1_38_1","unstructured":"Xujie Si Hanjun Dai Mukund Raghothaman Mayur Naik and Le Song. 2018. Learning loop invariants for program verification. In Neural Information Processing Systems."},{"key":"e_1_3_2_1_39_1","first-page":"801","article-title":"Sur la division des corps mat\u00e9riels en parties","volume":"1","author":"Hugo Steinhaus","year":"1956","unstructured":"Hugo Steinhaus et al. 1956. Sur la division des corps mat\u00e9riels en parties. Bull. Acad. Polon. Sci 1, 804 (1956), 801.","journal-title":"Bull. Acad. Polon. Sci"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_32"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409752"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"}],"event":{"name":"ICSE '22: 44th International Conference on Software Engineering","location":"Pittsburgh Pennsylvania","acronym":"ICSE '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 44th International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3510003.3510220","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3510003.3510220","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:12:24Z","timestamp":1750191144000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3510003.3510220"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,21]]},"references-count":43,"alternative-id":["10.1145\/3510003.3510220","10.1145\/3510003"],"URL":"https:\/\/doi.org\/10.1145\/3510003.3510220","relation":{},"subject":[],"published":{"date-parts":[[2022,5,21]]},"assertion":[{"value":"2022-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}