{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:28:44Z","timestamp":1769732924628,"version":"3.49.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032068460","type":"print"},{"value":"9783032068477","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-06847-7_5","type":"book-chapter","created":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:27Z","timestamp":1761954147000},"page":"88-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Accelerating CAR-Based Model-Checking with\u00a0Multiple Unsatisfiable Cores"],"prefix":"10.1007","author":[{"given":"Yibo","family":"Dong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiwei","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,1]]},"reference":[{"key":"5_CR1","unstructured":"ABC: System for Sequential Logic Synthesis and Formal Verification. https:\/\/github.com\/berkeley-abc\/abc"},{"key":"5_CR2","unstructured":"AVY. https:\/\/arieg.bitbucket.io\/avy\/"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Bernardini, A., Ecker, W., Schlichtmann, U.: Where formal verification can help in functional safety analysis. In: IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp.\u00a01\u20138 (2016). https:\/\/doi.org\/10.1145\/2966986.2980087","DOI":"10.1145\/2966986.2980087"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of Design Automation Conference (DAC), pp. 317\u2013320 (1999). https:\/\/doi.org\/10.1109\/DAC.1999.781333","DOI":"10.1109\/DAC.1999.781333"},{"key":"5_CR5","unstructured":"Biere, A.: AIGER Format. http:\/\/fmv.jku.at\/aiger\/FORMAT"},{"key":"5_CR6","first-page":"193","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 193\u2013207. Springer, Berlin, Heidelberg (1999)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 70\u201387. Springer, Berlin, Heidelberg (2011)"},{"issue":"2","key":"5_CR8","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Inf. Comput."},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Dong, Y.: mUC-artifact (2025). https:\/\/doi.org\/10.5281\/zenodo.15227232","DOI":"10.5281\/zenodo.15227232"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Dureja, R., Li, J., Pu, G., Vardi, M.Y., Rozier, K.Y.: Intersection and rotation of assumption literals boosts bug-finding. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments, pp. 180\u2013192. Springer International Publishing, Cham (2020)","DOI":"10.1007\/978-3-030-41600-3_12"},{"key":"5_CR11","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pp. 125\u2013134. FMCAD \u201911, FMCAD Inc, Austin, Texas (2011)"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, pp. 502\u2013518. Springer, Berlin, Heidelberg (2004)"},{"key":"5_CR13","unstructured":"HWMCC 2024. https:\/\/hwmcc.github.io\/2024\/"},{"key":"5_CR14","unstructured":"IC3Ref. https:\/\/github.com\/arbrad\/IC3ref"},{"issue":"4","key":"5_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. (CSUR) 41(4), 1\u201354 (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-96142-2_5","volume-title":"Computer Aided Verification","author":"J Li","year":"2018","unstructured":"Li, J., Dureja, R., Pu, G., Rozier, K.Y., Vardi, M.Y.: SimpleCAR: an efficient bug-finding tool based on approximate reachability. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 37\u201344. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_5"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Li, J., Zhu, S., Zhang, Y., Pu, G., Vardi, M.Y.: Safety model checking with complementary approximations. In: 2017 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 95\u2013100 (2017). https:\/\/doi.org\/10.1109\/ICCAD.2017.8203765","DOI":"10.1109\/ICCAD.2017.8203765"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) Computer Aided Verification, pp. 1\u201313. Springer, Berlin, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference (DAC\u201901) (2001)","DOI":"10.1145\/378239.379017"},{"key":"5_CR20","unstructured":"NAVY. https:\/\/bitbucket.org\/arieg\/extavy\/downloads\/fib_cav15.tar.gz"},{"key":"5_CR21","unstructured":"nuXmv with i-good Lemmas. https:\/\/github.com\/youyusama\/i-Good_Lemmas_MC"},{"key":"5_CR22","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-030-94583-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Seufert","year":"2022","unstructured":"Seufert, T., Scholl, C., Chandrasekharan, A., Reimer, S., Welp, T.: Making PROGRESS in property directed reachability. In: Finkbeiner, B., Wies, T. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 355\u2013377. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_18"},{"key":"5_CR23","unstructured":"SimpleCAR. https:\/\/github.com\/lijwen2748\/simplecar\/releases\/tag\/v0.1 (2018)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: International Conference on Computer Aided Verification, pp. 260\u2013276. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Vizel, Y., Gurfinkel, A., Malik, S.: Fast interpolating BMC. In: Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I 27, pp. 641\u2013657. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_43"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Xia, Y., Becchi, A., Cimatti, A., Griggio, A., Li, J., Pu, G.: Searching for i-good lemmas to accelerate safety model checking. In: International Conference on Computer Aided Verification, pp. 288\u2013308. Springer (2023)","DOI":"10.1007\/978-3-031-37703-7_14"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Zhang, X., Xiao, S., Li, J., Pu, G., Strichman, O.: Combining BMC and complementary approximate reachability to accelerate bug-finding. In: Proceedings of the 41st IEEE\/ACM International Conference on Computer-Aided Design. ICCAD \u201922, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3508352.3549393","DOI":"10.1145\/3508352.3549393"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06847-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:29Z","timestamp":1761954149000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06847-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,1]]},"ISBN":["9783032068460","9783032068477"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06847-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,1]]},"assertion":[{"value":"1 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}