{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T12:12:09Z","timestamp":1781007129717,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,31]]},"DOI":"10.1145\/3672608.3707984","type":"proceedings-article","created":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:26:21Z","timestamp":1747247181000},"page":"1721-1729","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["LLM-guided Predicate Discovery and Data Augmentation for Learning Likely Program Invariants"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0649-3101","authenticated-orcid":false,"given":"Yuan","family":"Xia","sequence":"first","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-1935-4533","authenticated-orcid":false,"given":"Aabha","family":"Pingle","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2361-9761","authenticated-orcid":false,"given":"Deepayan","family":"Sur","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4683-5540","authenticated-orcid":false,"given":"Jyotirmoy","family":"Deshmukh","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2879-0932","authenticated-orcid":false,"given":"Mukund","family":"Raghothaman","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2965-3940","authenticated-orcid":false,"given":"Srivatsan","family":"Ravi","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,5,14]]},"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","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_3_2_1_3_1","first-page":"1681","article-title":"Survey of dynamic analysis based program invariant synthesis techniques","volume":"31","author":"Bo Wang","year":"2020","unstructured":"Wang Bo, Lu Si-Rui, Jiang Jia-Jun, and Xiong Ying-Fei. 2020. Survey of dynamic analysis based program invariant synthesis techniques. In Journal of Software, Vol. 31. 1681\u20131702.","journal-title":"Journal of Software"},{"key":"e_1_3_2_1_4_1","volume-title":"Bradley and Zohar Manna","author":"Aaron","year":"2008","unstructured":"Aaron R. Bradley and Zohar Manna. 2008. Property-directed incremental invariant generation. In Formal aspects of computing, Vol. 20. Springer, 379\u2013405."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.747866"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092730"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TMEE.2011.6199191"},{"key":"e_1_3_2_1_8_1","volume-title":"Science of computer programming","author":"Ernst Michael D","unstructured":"Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant, Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. In Science of computer programming, Vol. 69. Elsevier, 35\u201345."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2012.6338671"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_14"},{"key":"e_1_3_2_1_12_1","volume-title":"Formal methods in system design","author":"Fedyukovich Grigory","unstructured":"Grigory Fedyukovich, Samuel J Kaufman, and Rastislav Bod\u00edk. 2020. Learning inductive invariants by sampling from frequency distributions. In Formal methods in system design, Vol. 56. Springer, 154\u2013177."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_16_1","volume-title":"The model checker SPIN","author":"Holzmann Gerard J.","unstructured":"Gerard J. Holzmann. 1997. The model checker SPIN. In IEEE Transactions on software engineering, Vol. 23. IEEE, 279\u2013295."},{"key":"e_1_3_2_1_17_1","volume-title":"Design and validation of computer protocols","author":"Holzmann Gerard J","unstructured":"Gerard J Holzmann and William Slattery Lieberman. 1991. Design and validation of computer protocols. Vol. 512. Prentice hall Englewood Cliffs."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.95"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1401827.1401839"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534381"},{"key":"e_1_3_2_1_22_1","volume-title":"The journal of logic and algebraic programming","author":"Leucker Martin","unstructured":"Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification. In The journal of logic and algebraic programming, Vol. 78. Elsevier, 293\u2013303."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155660"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_2_1_25_1","volume-title":"Journal of Automated Reasoning","author":"Neider Daniel","unstructured":"Daniel Neider, Parthasarathy Madhusudan, Shambwaditya Saha, Pranav Garg, and Daejun Park. 2020. A learning-based approach to synthesizing invariants for incomplete verification engines. In Journal of Automated Reasoning, Vol. 64. Springer, 1523\u20131552."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908099"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_7"},{"key":"e_1_3_2_1_31_1","unstructured":"Elizabeth Polgreen Ralph Abboud and Daniel Kroening. 2020. Counterexample guided neural synthesis. In arXiv preprint arXiv:2001.09245."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2010.5609576"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.22215\/etd\/2014-10300"},{"key":"e_1_3_2_1_34_1","unstructured":"Gabriel Ryan Justin Wong Jianan Yao Ronghui Gu and Suman Jana. 2019. CLN2INV: learning loop invariants with continuous logic networks. In arXiv preprint arXiv:1909.11542."},{"key":"e_1_3_2_1_35_1","unstructured":"Gagan Sharma. 2022. SPIN Model Checker Programs. https:\/\/github.com\/gagansh7171\/SPIN-Model-Checker-Programs\/tree\/master."},{"key":"e_1_3_2_1_36_1","volume-title":"Formal Methods in System Design","author":"Sharma Rahul","unstructured":"Rahul Sharma and Alex Aiken. 2016. From invariant checking to invariant inference using randomized search. In Formal Methods in System Design, Vol. 48. Springer, 235\u2013256."},{"key":"e_1_3_2_1_37_1","volume-title":"Programming Languages and Systems: 22nd European Symposium on Programming, ESOP, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS","author":"Sharma Rahul","unstructured":"Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya V Nori. 2013. A data driven approach for algebraic loop invariants. In Programming Languages and Systems: 22nd European Symposium on Programming, ESOP, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Rome, Italy, March 16\u201324. Proc. 22. Springer, 574\u2013592."},{"key":"e_1_3_2_1_38_1","volume-title":"Advances in Neural Information Processing Systems","volume":"31","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, Vol. 31."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_9"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462174"},{"key":"e_1_3_2_1_41_1","volume-title":"Jyotirmoy Deshmukh, Mukund Raghothaman, and Srivatsan Ravi.","author":"Xia Yuan","year":"2025","unstructured":"Yuan Xia, Deepayan Sur, Aabha Shailesh Pingle, Jyotirmoy Deshmukh, Mukund Raghothaman, and Srivatsan Ravi. 2025. Discovering Likely Invariants and Anomalies in Distributed Systems through Runtime Monitoring and Learning. In To appear in 26th International Conference on Verification, Model Checking, and Abstract Interpretation."},{"key":"e_1_3_2_1_42_1","volume-title":"Electronics","volume":"11","author":"Yang Zhe","year":"2022","unstructured":"Zhe Yang, Meiyi Dai, and Jian Guo. 2022. Formal modeling and verification of smart contracts with SPIN. In Electronics, Vol. 11. MDPI, 3091."},{"key":"e_1_3_2_1_43_1","volume-title":"Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). 485\u2013501."},{"key":"e_1_3_2_1_44_1","volume-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 405\u2013421."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"}],"event":{"name":"SAC '25: 40th ACM\/SIGAPP Symposium on Applied Computing","location":"Catania International Airport Catania Italy","acronym":"SAC '25","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"]},"container-title":["Proceedings of the 40th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707984","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3672608.3707984","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:37Z","timestamp":1750298257000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707984"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":45,"alternative-id":["10.1145\/3672608.3707984","10.1145\/3672608"],"URL":"https:\/\/doi.org\/10.1145\/3672608.3707984","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]},"assertion":[{"value":"2025-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}