{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T09:47:11Z","timestamp":1785577631871,"version":"3.56.0"},"publisher-location":"New York, NY, USA","reference-count":72,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,10]],"date-time":"2022-10-10T00:00:00Z","timestamp":1665360000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,10,10]]},"DOI":"10.1145\/3551349.3556942","type":"proceedings-article","created":{"date-parts":[[2023,1,5]],"date-time":"2023-01-05T20:43:54Z","timestamp":1672951434000},"page":"1-12","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Learning to Synthesize Relational Invariants"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0001-5877-2677","authenticated-orcid":false,"given":"Jingbo","family":"Wang","sequence":"first","affiliation":[{"name":"University of Southern California, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Southern California, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,5]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"11","article-title":"Improving the structure of loop nests in scientific programs","volume":"19","author":"Abdelrahman S","year":"2004","unstructured":"Tarek\u00a0S Abdelrahman and Robert Sawaya. 2004. Improving the structure of loop nests in scientific programs. Comput. Syst. Sci. Eng. 19, 1 (2004), 11\u201325.","journal-title":"Comput. Syst. Sci. Eng."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_8"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062378"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/197405.197406"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978427"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_28"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"e_1_3_2_1_10_1","volume-title":"Leveraging Grammar and Reinforcement Learning for Neural Program Synthesis. In International Conference on Learning Representations.","author":"Bunel Rudy","year":"2018","unstructured":"Rudy Bunel, Matthew Hausknecht, Jacob Devlin, Rishabh Singh, and Pushmeet Kohli. 2018. Leveraging Grammar and Reinforcement Learning for Neural Program Synthesis. In International Conference on Learning Representations."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134058"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360567"},{"key":"e_1_3_2_1_15_1","volume-title":"Program Synthesis Using Deduction-Guided Reinforcement Learning. In International Conference on Computer Aided Verification. Springer, 587\u2013610","author":"Chen Yanju","year":"2020","unstructured":"Yanju Chen, Chenglong Wang, Osbert Bastani, Isil Dillig, and Yu Feng. 2020. Program Synthesis Using Deduction-Guided Reinforcement Learning. In International Conference on Computer Aided Verification. Springer, 587\u2013610."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_46"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509511"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_19"},{"key":"e_1_3_2_1_21_1","volume-title":"Compositional recurrence analysis. In 2015 Formal Methods in Computer-Aided Design (FMCAD)","author":"Farzan Azadeh","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional recurrence analysis. In 2015 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 57\u201364."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192382"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062351"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837629"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837664"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_18"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-015-0100-7"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the ACM on Programming Languages 4, POPL(2019)","author":"Guo Zheng","year":"2019","unstructured":"Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. 2019. Program synthesis by type-guided abstraction refinement. Proceedings of the ACM on Programming Languages 4, POPL(2019), 1\u201328."},{"key":"e_1_3_2_1_32_1","unstructured":"Travis Hance Marijn Heule Ruben Martins and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019s a Small (Enough) World After All.. In NSDI. 115\u2013131."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_1_35_1","volume-title":"The ELDARICA horn solver. In 2018 Formal Methods in Computer Aided Design (FMCAD)","author":"Hojjat Hossein","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The ELDARICA horn solver. In 2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 1\u20137."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062373"},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL(2017)","author":"Kincaid Zachary","year":"2017","unstructured":"Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. 2017. Non-linear reasoning for invariant synthesis. Proceedings of the ACM on Programming Languages 2, POPL(2017), 1\u201333."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542513"},{"key":"e_1_3_2_1_40_1","unstructured":"Chen Liang Mohammad Norouzi Jonathan Berant Quoc\u00a0V Le and Ni Lao. 2018. Memory Augmented Policy Optimization for Program Synthesis and Semantic Parsing. In NeurIPS."},{"key":"e_1_3_2_1_41_1","unstructured":"Jiayuan Mao Chuang Gan Pushmeet Kohli Joshua\u00a0B Tenenbaum and Jiajun Wu. 2019. The neuro-symbolic concept learner: Interpreting scenes words and sentences from natural supervision. arXiv preprint arXiv:1904.12584(2019)."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_16"},{"key":"e_1_3_2_1_43_1","volume-title":"Property directed inference of relational invariants. In 2019 Formal Methods in Computer Aided Design (FMCAD)","author":"Mordvinov Dmitry","unstructured":"Dmitry Mordvinov and Grigory Fedyukovich. 2019. Property directed inference of relational invariants. In 2019 Formal Methods in Computer Aided Design (FMCAD). IEEE, 152\u2013160."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2556782"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2738007"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908099"},{"key":"e_1_3_2_1_49_1","volume-title":"Loopinvgen: A loop invariant generator based on precondition inference. arXiv preprint arXiv:1707.02029(2017).","author":"Padhi Saswat","year":"2017","unstructured":"Saswat Padhi, Rahul Sharma, and Todd Millstein. 2017. Loopinvgen: A loop invariant generator based on precondition inference. arXiv preprint arXiv:1707.02029(2017)."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.34"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_9"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908093"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_9"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"e_1_3_2_1_57_1","unstructured":"Gabriel Ryan Justin Wong Jianan Yao Ronghui Gu and Suman Jana. 2019. CLN2INV: learning loop invariants with continuous logic networks. arXiv preprint arXiv:1909.11542(2019)."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0248-5"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"e_1_3_2_1_63_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_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_9"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_1_66_1","volume-title":"Reinforcement learning: An introduction","author":"Sutton S","unstructured":"Richard\u00a0S Sutton and Andrew\u00a0G Barto. 2018. Reinforcement learning: An introduction. MIT press."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_1_68_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL(2017)","author":"Wang Xinyu","year":"2017","unstructured":"Xinyu Wang, Isil Dillig, and Rishabh Singh. 2017. Program synthesis using abstraction refinement. Proceedings of the ACM on Programming Languages 2, POPL(2017), 1\u201330."},{"key":"e_1_3_2_1_69_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL(2017)","author":"Wang Yuepeng","year":"2017","unstructured":"Yuepeng Wang, Isil Dillig, Shuvendu\u00a0K Lahiri, and William\u00a0R Cook. 2017. Verifying equivalence of database-driven applications. Proceedings of the ACM on Programming Languages 2, POPL(2017), 1\u201329."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192416"}],"event":{"name":"ASE '22: 37th IEEE\/ACM International Conference on Automated Software Engineering","location":"Rochester MI USA","acronym":"ASE '22"},"container-title":["Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3551349.3556942","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/3551349.3556942","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T08:29:25Z","timestamp":1755851365000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3551349.3556942"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,10]]},"references-count":72,"alternative-id":["10.1145\/3551349.3556942","10.1145\/3551349"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/3551349.3556942","relation":{},"subject":[],"published":{"date-parts":[[2022,10,10]]},"assertion":[{"value":"2023-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}