{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T03:59:11Z","timestamp":1769745551489,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":12,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T00:00:00Z","timestamp":1719100800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Basic Research Projects from the Institute of Software, Chinese Academy of Sciences","award":["ISCAS-JCZD-202307"],"award-info":[{"award-number":["ISCAS-JCZD-202307"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62372438"],"award-info":[{"award-number":["62372438"]}],"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":[[2024,6,23]]},"DOI":"10.1145\/3649329.3655970","type":"proceedings-article","created":{"date-parts":[[2024,11,7]],"date-time":"2024-11-07T19:27:22Z","timestamp":1731007642000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Predicting Lemmas in Generalization of IC3"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-2571-8135","authenticated-orcid":false,"given":"Yuheng","family":"Su","sequence":"first","affiliation":[{"name":"University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8099-2035","authenticated-orcid":false,"given":"Qiusong","family":"Yang","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1897-7536","authenticated-orcid":false,"given":"Yiwei","family":"Ci","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2023. ABC. https:\/\/github.com\/berkeley-abc\/abc."},{"key":"e_1_3_2_1_2_1","unstructured":"2023. CAV23 Artifact. https:\/\/github.com\/youyusama\/i-Good_Lemmas_MC."},{"key":"e_1_3_2_1_3_1","unstructured":"2023. IC3ref. https:\/\/github.com\/arbrad\/IC3ref."},{"key":"e_1_3_2_1_4_1","volume-title":"https:\/\/github.com\/gipsyh\/DAC24","author":"Artifact Reproductive","unstructured":"2023. Reproductive Artifact. https:\/\/github.com\/gipsyh\/DAC24."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_1_6_1","unstructured":"Niklas Een Alan Mishchenko and Robert Brayton. 2011. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD). 125--134."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Zyad Hassan Aaron R. Bradley and Fabio Somenzi. 2013. Better generalization in IC3. In 2013 Formal Methods in Computer-Aided Design. 157--164. 10.1109\/FMCAD.2013.6679405","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Alexander Ivrii and Arie Gurfinkel. 2015. Pushing to the top. In 2015 Formal Methods in Computer-Aided Design (FMCAD). 65--72.","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"e_1_3_2_1_9_1","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_3_2_1_10_1","volume-title":"Automation Test in Europe Conference Exhibition (DATE). 456--461","author":"Seufert Tobias","year":"2019","unstructured":"Tobias Seufert and Christoph Scholl. 2019. fbPDR: In-depth combination of forward and backward analysis in Property Directed Reachability. In 2019 Design, Automation Test in Europe Conference Exhibition (DATE). 456--461."},{"key":"e_1_3_2_1_11_1","volume-title":"Making PROGRESS in Property Directed Reachability","author":"Seufert Tobias","unstructured":"Tobias Seufert, Christoph Scholl, Arun Chandrasekharan, Sven Reimer, and Tobias Welp. 2022. Making PROGRESS in Property Directed Reachability. In Verification, Model Checking, and Abstract Interpretation, Bernd Finkbeiner and Thomas Wies (Eds.). Springer International Publishing, Cham, 355--377."},{"key":"e_1_3_2_1_12_1","volume-title":"Computer Aided Verification","author":"Xia Yechuan","unstructured":"Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, and Geguang Pu. 2023. Searching for i-Good Lemmas to Accelerate Safety Model Checking. In Computer Aided Verification. Springer Nature Switzerland, Cham, 288--308."}],"event":{"name":"DAC '24: 61st ACM\/IEEE Design Automation Conference","location":"San Francisco CA USA","acronym":"DAC '24","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE-CEDA","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 61st ACM\/IEEE Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3655970","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649329.3655970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:55Z","timestamp":1750295875000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3655970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,23]]},"references-count":12,"alternative-id":["10.1145\/3649329.3655970","10.1145\/3649329"],"URL":"https:\/\/doi.org\/10.1145\/3649329.3655970","relation":{},"subject":[],"published":{"date-parts":[[2024,6,23]]},"assertion":[{"value":"2024-11-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}