{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:00:18Z","timestamp":1750309218047,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,10,27]]},"DOI":"10.1145\/3676536.3676686","type":"proceedings-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:26:26Z","timestamp":1744205186000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Word-Level Augmentation of Formal Proof by Learning from Simulation Traces"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3857-6649","authenticated-orcid":false,"given":"Zhiyuan","family":"Yan","sequence":"first","affiliation":[{"name":"Microelectronics Thrust, Function Hub, The Hong Kong Univeristy of Science and Technology(Guangzhou), Guangzhou, Guangdong, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4001-264X","authenticated-orcid":false,"given":"Hongce","family":"Zhang","sequence":"additional","affiliation":[{"name":"Microelectronics Thrust, Function Hub, The Hong Kong Univeristy of Science and Technology(Guangzhou), Guangzhou, Guangdong, China"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"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":"Sygus-comp 2017: Results and analysis. arXiv preprint arXiv:1711.11438","author":"Alur Rajeev","year":"2017","unstructured":"Rajeev Alur, Dana Fisman, Rishabh Singh, and Armando Solar-Lezama. 2017. Sygus-comp 2017: Results and analysis. arXiv preprint arXiv:1711.11438 (2017)."},{"key":"e_1_3_2_1_3_1","volume-title":"Deepcoder: Learning to write programs. arXiv preprint arXiv:1611.01989","author":"Balog Matej","year":"2016","unstructured":"Matej Balog, Alexander L Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. 2016. Deepcoder: Learning to write programs. arXiv preprint arXiv:1611.01989 (2016)."},{"volume-title":"Satisfiability modulo theories","author":"Barrett Clark","key":"e_1_3_2_1_4_1","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. Springer."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems: 5th International Conference TACAS'99 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS'99 Amsterdam The Netherlands March 22--28 1999 Proceedings 5. Springer 193--207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_1_6_1","volume-title":"Leveraging grammar and reinforcement learning for neural program synthesis. arXiv preprint arXiv:1805.04276","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. arXiv preprint arXiv:1805.04276 (2018)."},{"key":"e_1_3_2_1_7_1","volume-title":"Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al.","author":"Chen Mark","year":"2021","unstructured":"Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. 2021. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021)."},{"key":"e_1_3_2_1_8_1","volume-title":"Towards synthesizing complex programs from input-output examples. arXiv preprint arXiv:1706.01284","author":"Chen Xinyun","year":"2017","unstructured":"Xinyun Chen, Chang Liu, and Dawn Song. 2017. Towards synthesizing complex programs from input-output examples. arXiv preprint arXiv:1706.01284 (2017)."},{"key":"e_1_3_2_1_9_1","volume-title":"International Conference on Learning Representations.","author":"Chen Xinyun","year":"2018","unstructured":"Xinyun Chen, Chang Liu, and Dawn Song. 2018. Execution-guided neural program synthesis. In International Conference on Learning Representations."},{"key":"e_1_3_2_1_10_1","first-page":"22196","article-title":"Latent execution for neural program synthesis beyond domain-specific languages","volume":"34","author":"Chen Xinyun","year":"2021","unstructured":"Xinyun Chen, Dawn Song, and Yuandong Tian. 2021. Latent execution for neural program synthesis beyond domain-specific languages. Advances in Neural Information Processing Systems 34 (2021), 22196--22208.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_30"},{"key":"e_1_3_2_1_12_1","volume-title":"Caglar Gulcehre, Dzmitry Bahdanau, Fethi Bougares, Holger Schwenk, and Yoshua Bengio.","author":"Cho Kyunghyun","year":"2014","unstructured":"Kyunghyun Cho, Bart Van Merri\u00ebnboer, Caglar Gulcehre, Dzmitry Bahdanau, Fethi Bougares, Holger Schwenk, and Yoshua Bengio. 2014. Learning phrase representations using RNN encoder-decoder for statistical machine translation. arXiv preprint arXiv:1406.1078 (2014)."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3061639.3062206"},{"key":"e_1_3_2_1_15_1","volume-title":"International conference on machine learning. PMLR, 990--998","author":"Devlin Jacob","year":"2017","unstructured":"Jacob Devlin, Jonathan Uesato, Surya Bhupatiraju, Rishabh Singh, Abdel-rahman Mohamed, and Pushmeet Kohli. 2017. Robustfill: Neural program learning under noisy i\/o. In International conference on machine learning. PMLR, 990--998."},{"volume-title":"Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD)","author":"E\u00e9n Niklas","key":"e_1_3_2_1_16_1","unstructured":"Niklas E\u00e9n, Alan Mishchenko, and Robert Brayton. 2011. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 125--134."},{"volume-title":"Assertion-based design","author":"Foster Harry D","key":"e_1_3_2_1_17_1","unstructured":"Harry D Foster, Adam C Krolnik, and David J Lacey. 2004. Assertion-based design. Springer Science & Business Media."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2022.3197525"},{"key":"e_1_3_2_1_19_1","volume-title":"International conference on machine learning. PMLR, 1263--1272","author":"Gilmer Justin","year":"2017","unstructured":"Justin Gilmer, Samuel S Schoenholz, Patrick F Riley, Oriol Vinyals, and George E Dahl. 2017. Neural message passing for quantum chemistry. In International conference on machine learning. PMLR, 1263--1272."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v32i1.11694"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622737.1622748"},{"key":"e_1_3_2_1_24_1","unstructured":"You Li. 2022. https:\/\/github.com\/you-li-nu\/hls_bench"},{"key":"e_1_3_2_1_25_1","volume-title":"Gated graph sequence neural networks. arXiv preprint arXiv:1511.05493","author":"Li Yujia","year":"2015","unstructured":"Yujia Li, Daniel Tarlow, Marc Brockschmidt, and Richard Zemel. 2015. Gated graph sequence neural networks. arXiv preprint arXiv:1511.05493 (2015)."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC56929.2023.10247912"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429384.2429424"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970526"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_22"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_1"},{"key":"e_1_3_2_1_32_1","volume-title":"International conference on machine learning. PMLR","author":"Mnih Volodymyr","year":"2016","unstructured":"Volodymyr Mnih, Adria Puigdomenech Badia, Mehdi Mirza, Alex Graves, Timothy Lillicrap, Tim Harley, David Silver, and Koray Kavukcuoglu. 2016. Asynchronous methods for deep reinforcement learning. In International conference on machine learning. PMLR, 1928--1937."},{"key":"e_1_3_2_1_33_1","volume-title":"Neuro-symbolic program synthesis. arXiv preprint arXiv:1611.01855","author":"Parisotto Emilio","year":"2016","unstructured":"Emilio Parisotto, Abdel-rahman Mohamed, Rishabh Singh, Lihong Li, Dengyong Zhou, and Pushmeet Kohli. 2016. Neuro-symbolic program synthesis. arXiv preprint arXiv:1611.01855 (2016)."},{"key":"e_1_3_2_1_34_1","volume-title":"Hardware model checking competition","author":"Preiner Mathias","year":"2020","unstructured":"Mathias Preiner, Armin Biere, and Nils Froleyks. 2020. Hardware model checking competition 2020. (2020)."},{"key":"e_1_3_2_1_35_1","unstructured":"PyTorch. [n. d.]. ADAPTIVEAVGPOOL2D. https:\/\/pytorch.org\/docs\/stable\/generated\/torch.nn.AdaptiveAvgPool2d.html#torch.nn.AdaptiveAvgPool2d"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2014.19"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_9"},{"key":"e_1_3_2_1_39_1","volume-title":"International Conference on Learning Representations.","author":"Si Xujie","year":"2019","unstructured":"Xujie Si, Yuan Yang, Hanjun Dai, Mayur Naik, and Le Song. 2019. Learning a meta-solver for syntax-guided program synthesis. In International Conference on Learning Representations."},{"key":"e_1_3_2_1_40_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE","author":"Vasudevan Shobha","year":"2010","unstructured":"Shobha Vasudevan, David Sheridan, Sanjay Patel, David Tcheng, Bill Tuohy, and Daniel Johnson. 2010. Goldmine: Automatic assertion generation using data mining and static analysis. In 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010). IEEE, 626--629."},{"key":"e_1_3_2_1_41_1","volume-title":"Attention is all you need. Advances in neural information processing systems 30","author":"Vaswani Ashish","year":"2017","unstructured":"Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, \u0141ukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. Advances in neural information processing systems 30 (2017)."},{"key":"e_1_3_2_1_42_1","volume-title":"2020 IEEE\/ACM International Conference On Computer Aided Design (ICCAD). IEEE, 1--9.","author":"Grigory Fedyukovich Hari Govind VK","year":"2020","unstructured":"Hari Govind VK, Grigory Fedyukovich, and Arie Gurfinkel. 2020. Word level property directed reachability. In 2020 IEEE\/ACM International Conference On Computer Aided Design (ICCAD). IEEE, 1--9."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510578"},{"key":"e_1_3_2_1_44_1","volume-title":"Deep Reinforcement Learning Guided Decision Tree Learning For Program Synthesis. In 2023 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE, 925--932","author":"Yang Mingrui","year":"2023","unstructured":"Mingrui Yang and Dalin Zhang. 2023. Deep Reinforcement Learning Guided Decision Tree Learning For Program Synthesis. In 2023 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE, 925--932."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_15"}],"event":{"name":"ICCAD '24: 43rd IEEE\/ACM International Conference on Computer-Aided Design","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA","IEEE EDS"],"location":"Newark Liberty International Airport Marriott New York NY USA","acronym":"ICCAD '24"},"container-title":["Proceedings of the 43rd IEEE\/ACM International Conference on Computer-Aided Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676536.3676686","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676536.3676686","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:43:57Z","timestamp":1750290237000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676536.3676686"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,27]]},"references-count":45,"alternative-id":["10.1145\/3676536.3676686","10.1145\/3676536"],"URL":"https:\/\/doi.org\/10.1145\/3676536.3676686","relation":{},"subject":[],"published":{"date-parts":[[2024,10,27]]},"assertion":[{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}