{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T00:35:24Z","timestamp":1773189324256,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T00:00:00Z","timestamp":1689120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62032024"],"award-info":[{"award-number":["62032024"]}],"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":[[2023,7,12]]},"DOI":"10.1145\/3597926.3598047","type":"proceedings-article","created":{"date-parts":[[2023,7,13]],"date-time":"2023-07-13T20:12:53Z","timestamp":1689279173000},"page":"175-187","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Loop Invariant Inference through SMT Solving Enhanced Reinforcement Learning"],"prefix":"10.1145","author":[{"given":"Shiwen","family":"Yu","sequence":"first","affiliation":[{"name":"National University of Defense Technology, China"}]},{"given":"Ting","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, China"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, China"}]}],"member":"320","published-online":{"date-parts":[[2023,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.260.9"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_25"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_19"},{"key":"e_1_3_2_1_5_1","volume-title":"Johnson","author":"Caviness B. F.","year":"1998","unstructured":"B. F. Caviness and Jeremy R . Johnson . 1998 . Quantifier Elimination and Cylindrical Algebraic Decomposition. In Texts and Monographs in Symbolic Computation . B. F. Caviness and Jeremy R. Johnson. 1998. Quantifier Elimination and Cylindrical Algebraic Decomposition. In Texts and Monographs in Symbolic Computation."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1142\/12360"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_7"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115689"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115690"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_10"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115691"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2556782"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSME55016.2022.00031"},{"key":"e_1_3_2_1_30_1","volume-title":"Language to Specify Syntax-Guided Synthesis Problems. CoRR, abs\/1405.5590","author":"Raghothaman Mukund","year":"2014","unstructured":"Mukund Raghothaman and Abhishek Udupa . 2014. Language to Specify Syntax-Guided Synthesis Problems. CoRR, abs\/1405.5590 ( 2014 ), arXiv:1405.5590. arxiv:1405.5590 Mukund Raghothaman and Abhishek Udupa. 2014. Language to Specify Syntax-Guided Synthesis Problems. CoRR, abs\/1405.5590 (2014), arXiv:1405.5590. arxiv:1405.5590"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549166"},{"key":"e_1_3_2_1_32_1","volume-title":"8th International Conference on Learning Representations, ICLR 2020","author":"Ryan Gabriel","year":"2020","unstructured":"Gabriel Ryan , Justin Wong , Jianan Yao , Ronghui Gu , and Suman Jana . 2020 . CLN2INV: Learning Loop Invariants with Continuous Logic Networks . In 8th International Conference on Learning Representations, ICLR 2020 , Addis Ababa, Ethiopia , April 26-30, 2020. OpenReview.net. https:\/\/openreview.net\/forum?id=HJlfuTEtvB Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020. CLN2INV: Learning Loop Invariants with Continuous Logic Networks. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net. https:\/\/openreview.net\/forum?id=HJlfuTEtvB"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_3_2_1_36_1","volume-title":"Learning Loop Invariants for Program Verification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018","author":"Si Xujie","year":"2018","unstructured":"Xujie Si , Hanjun Dai , Mukund Raghothaman , Mayur Naik , and Le Song . 2018 . Learning Loop Invariants for Program Verification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 , NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, and Roman Garnett (Eds.). 7762\u20137773. https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/65b1e92c585fd4c2159d5f33b5030ff2-Abstract.html Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. 2018. Learning Loop Invariants for Program Verification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, and Roman Garnett (Eds.). 7762\u20137773. https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/65b1e92c585fd4c2159d5f33b5030ff2-Abstract.html"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/p15-1150"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468567"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409752"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784766"}],"event":{"name":"ISSTA '23: 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Seattle WA USA","acronym":"ISSTA '23","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"]},"container-title":["Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597926.3598047","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3597926.3598047","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:41Z","timestamp":1750182521000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597926.3598047"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,12]]},"references-count":43,"alternative-id":["10.1145\/3597926.3598047","10.1145\/3597926"],"URL":"https:\/\/doi.org\/10.1145\/3597926.3598047","relation":{},"subject":[],"published":{"date-parts":[[2023,7,12]]},"assertion":[{"value":"2023-07-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}