{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T08:06:05Z","timestamp":1759565165692,"version":"3.37.3"},"reference-count":39,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"9","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program","doi-asserted-by":"publisher","award":["2020AAA0107800"],"award-info":[{"award-number":["2020AAA0107800"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Shanghai Collaborative Innovation Center of Trusted Industry Internet Software"},{"name":"Shanghai Pujiang Talent Plan","award":["20PJ1403500"],"award-info":[{"award-number":["20PJ1403500"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62002118","U21B2015"],"award-info":[{"award-number":["62002118","U21B2015"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2023,9]]},"DOI":"10.1109\/tcad.2023.3236272","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:11:17Z","timestamp":1673475077000},"page":"3105-3117","source":"Crossref","is-referenced-by-count":2,"title":["Accelerate Safety Model Checking Based on Complementary Approximate Reachability"],"prefix":"10.1109","volume":"42","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8125-754X","authenticated-orcid":false,"given":"Xiaoyu","family":"Zhang","sequence":"first","affiliation":[{"name":"Software Engineering Institute, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengping","family":"Xiao","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yechuan","family":"Xia","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-8285","authenticated-orcid":false,"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3922-0989","authenticated-orcid":false,"given":"Mingsong","family":"Chen","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9750-8334","authenticated-orcid":false,"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"journal-title":"HWMCC 2015","year":"2015","key":"ref13"},{"journal-title":"Artifact","year":"0","key":"ref35"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41600-3_12"},{"journal-title":"AIGER Format","year":"0","author":"biere","key":"ref34"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"journal-title":"IIMC","year":"2018","key":"ref37"},{"journal-title":"HWMCC 2017","year":"2017","key":"ref14"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"journal-title":"Minisat 2 2 0","year":"2013","key":"ref31"},{"key":"ref30","first-page":"502","article-title":"An extensible SAT-solver","author":"e\u00e9n","year":"0","journal-title":"Theory and Applications of Satisfiability Testing"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_30"},{"key":"ref33","first-page":"221","article-title":"Boosting minimal unsatisfiable core extraction","author":"nadel","year":"2010","journal-title":"Proc Conf Formal Methods Comput -Aided Des"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_5"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-2012-0523"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2966986.2980087"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_34"},{"journal-title":"Simple","year":"2018","key":"ref39"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13754-9_11"},{"journal-title":"IC3ref","year":"2015","key":"ref38"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_19"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_21"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/776038.776043"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2481869"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_15"},{"key":"ref27","first-page":"63","article-title":"IC3 with internal signals","author":"dureja","year":"2021","journal-title":"Proc Formal Methods Comput -Aided Des (FMCAD)"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_18"},{"key":"ref8","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"een","year":"2011","journal-title":"Proc Int Conf Formal Methods Comput -Aided Des"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2017.8203765"},{"key":"ref4","first-page":"317","article-title":"Symbolic model checking using SAT procedures instead of BDDs","author":"biere","year":"1999","journal-title":"Proc Des Autom Conf (DAC)"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/10225609\/10015642.pdf?arnumber=10015642","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T18:09:13Z","timestamp":1694455753000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10015642\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":39,"journal-issue":{"issue":"9"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2023.3236272","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"type":"print","value":"0278-0070"},{"type":"electronic","value":"1937-4151"}],"subject":[],"published":{"date-parts":[[2023,9]]}}}