{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:04:58Z","timestamp":1784797498189,"version":"3.55.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325365","type":"print"},{"value":"9783032325372","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We introduce a generic certificate format for verifying liveness properties in hardware model checking. The format relies purely on propositional predicates and does not involve explicit counters. Our certificates can be efficiently validated using a fixed number of SAT checks. The proposed format is compatible with state-of-the-art liveness checking algorithms. We present certificate generation for several representative techniques, including rLive, liveness-to-safety reduction, and\n                    <jats:italic>k<\/jats:italic>\n                    -liveness, as well as for a preprocessing method based on stabilizing constraint extraction. Experimental results on benchmarks from the Hardware Model Checking Competition demonstrate that our approach is practically effective with very low certification overhead, and our certificate checker successfully validated all generated certificates.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32537-2_1","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:41:41Z","timestamp":1784796101000},"page":"3-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Liveness Proofs for\u00a0Hardware Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3925-3438","authenticated-orcid":false,"given":"Nils","family":"Froleyks","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4993-773X","authenticated-orcid":false,"given":"Emily","family":"Yu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3460-4251","authenticated-orcid":false,"given":"Bart","family":"Bogaerts","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4547-2701","authenticated-orcid":false,"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Quantitative supermartingale certificates. In: International Conference on Computer Aided Verification, pp. 3\u201328. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_1","DOI":"10.1007\/978-3-031-98679-6_1"},{"issue":"4","key":"1_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","journal-title":"Inf. Process. Lett."},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Cleaveland, R., Garavel, H. (eds.) 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems, FMICS 2002, ICALP 2002 Satellite Workshop, M\u00e1laga, Spain, 12\u201313 July 2002. Electronic Notes in Theoretical Computer Science, vol. 66, pp. 160\u2013177. Elsevier (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80410-9","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT competition 2025. In: Codel, C., Fazekas, K., Heule, M., Iser, M. (eds.) Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions, p. 10. Proceedings of SAT Competitions, TU Wien Academic Press (2025). https:\/\/doi.org\/10.34726\/10379","DOI":"10.34726\/10379"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2025. In: Irfan, A., Kaufmann, D. (eds.) Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, 6\u201310 October 2025. TU Wien Academic Press (2025). https:\/\/doi.org\/10.34727\/2025\/ISBN.978-3-85448-084-6_6","DOI":"10.34727\/2025\/ISBN.978-3-85448-084-6_6"},{"key":"1_CR7","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"1_CR8","unstructured":"Biere, A., Herbstritt, M., Berre, D.L., Wieringa, S., Niemetz, A.: AIGER: and-inverter graph (AIG) format and tools. https:\/\/github.com\/arminbiere\/aiger (2006)"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: Understanding IC3. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 1\u201314. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_1","DOI":"10.1007\/978-3-642-31612-8_1"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: International Colloquium on Automata, Languages, and Programming, pp. 1349\u20131361. Springer (2005). https:\/\/doi.org\/10.1007\/11523468_109","DOI":"10.1007\/11523468_109"},{"key":"1_CR11","unstructured":"Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: 2011 Formal Methods in Computer-Aided Design (FMCAD), pp. 144\u2013153. IEEE (2011). http:\/\/dl.acm.org\/citation.cfm?id=2157677"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: International Conference on Computer Aided Verification, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"1_CR13","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 52\u201359. IEEE (2012). https:\/\/ieeexplore.ieee.org\/document\/6462555\/"},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/1190216.1190257","volume":"42","author":"B Cook","year":"2007","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. ACM SIGPLAN Notices 42(1), 265\u2013276 (2007). https:\/\/doi.org\/10.1145\/1190216.1190257","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety: (tool paper). In: International Conference on Computer Aided Verification, pp. 415\u2013418. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_37","DOI":"10.1007\/11817963_37"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: International Conference on Computer Aided Verification, pp. 49\u201366. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable LTL model checker. In: International Conference on Computer Aided Verification, pp. 463\u2013478. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_31","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Program Verification: Fundamental Issues in Computer Science, pp. 65\u201381. Springer (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"1_CR19","unstructured":"Froleyks, N., Yu, E.: Hardware model checking certification with Certifaiger and Cerbtora. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR) 2026, Part of FLoC 2026, Lisbon, Portugal, 26\u201329 July 2026. Lecture Notes in Computer Science, Springer, Lisbon, Portugal (2026)"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Yu, E., Biere, A., Heljanko, K.: Certifying phase abstraction. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, 3\u20136 July 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14739, pp. 284\u2013303. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_17","DOI":"10.1007\/978-3-031-63498-7_17"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Yu, E., Preiner, M., Biere, A., Heljanko, K.: Introducing certificates to the hardware model checking competition. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, 23\u201325 July 2025, Proceedings, Part I. Lecture Notes in Computer Science, vol. 15931, pp. 281\u2013295. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_14","DOI":"10.1007\/978-3-031-98668-0_14"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Gan, X., Dubrovin, J., Heljanko, K.: A symbolic model checking approach to verifying satellite onboard software. Sci. Comput. Program. 82, 44\u201355 (2014). https:\/\/doi.org\/10.1016\/J.SCICO.2013.03.005","DOI":"10.1016\/J.SCICO.2013.03.005"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Giacobbe, M., Kroening, D., Pal, A., Tautschnig, M.: Neural model checking. Adv. Neural. Inf. Process. Syst. 37, 86375\u201386398 (2024). https:\/\/doi.org\/10.52202\/079017-2742","DOI":"10.52202\/079017-2742"},{"key":"1_CR24","unstructured":"Giacobbe, M., Kroening, D., Pal, A., Tautschnig, M.: Let a neural network be your invariant. In: The Thirty-ninth Annual Conference on Neural Information Processing Systems (2025)"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pp. 1\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603022","DOI":"10.23919\/FMCAD.2018.8603022"},{"issue":"2","key":"1_CR26","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-021-00369-1","volume":"57","author":"A Griggio","year":"2021","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for SAT-based model checking. Formal Methods Syst. Design 57(2), 178\u2013210 (2021). https:\/\/doi.org\/10.1007\/s10703-021-00369-1","journal-title":"Formal Methods Syst. Design"},{"issue":"2","key":"1_CR27","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1016\/j.jcss.2011.05.004","volume":"78","author":"K Heljanko","year":"2012","unstructured":"Heljanko, K., Kein\u00e4nen, M., Lange, M., Niemel\u00e4, I.: Solving parity games by a reduction to SAT. J. Comput. Syst. Sci. 78(2), 430\u2013440 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.05.004","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: International Conference on Computer Aided Verification, pp. 89\u2013103. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_9","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Kuismin, T., Heljanko, K.: Increasing confidence in liveness model checking results with proofs. In: Haifa Verification Conference, pp. 32\u201343. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7_3","DOI":"10.1007\/978-3-319-03077-7_3"},{"issue":"8","key":"1_CR30","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1016\/J.IPL.2014.03.001","volume":"114","author":"GP Maretic","year":"2014","unstructured":"Maretic, G.P., Dashti, M.T., Basin, D.A.: LTL is closed under topological closure. Inf. Process. Lett. 114(8), 408\u2013413 (2014). https:\/\/doi.org\/10.1016\/J.IPL.2014.03.001","journal-title":"Inf. Process. Lett."},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Toward liveness proofs at scale. In: International Conference on Computer Aided Verification, pp. 255\u2013276. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_13","DOI":"10.1007\/978-3-031-65627-9_13"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: International Conference on Computer Aided Verification, pp. 190\u2013202. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Mebsout, A., Tinelli, C.: Proof certificates for SMT-based model checkers for infinite-state systems. In: FMCAD, pp. 117\u2013124. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886669","DOI":"10.1109\/FMCAD.2016.7886669"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Murali, V., Trivedi, A., Zamani, M.: Closure certificates. In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2024). https:\/\/doi.org\/10.1145\/3641513.3650120","DOI":"10.1145\/3641513.3650120"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2\u201313. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_2"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. In: Proceedings of the ACM on Programming Languages vol. 2, no. (POPL), pp. 1\u201333 (2017). https:\/\/doi.org\/10.1145\/3158114","DOI":"10.1145\/3158114"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004, pp. 32\u201341. IEEE (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319598","DOI":"10.1109\/LICS.2004.1319598"},{"issue":"1","key":"1_CR39","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1145\/1047659.1040317","volume":"40","author":"A Podelski","year":"2005","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM SIGPLAN Notices 40(1), 132\u2013144 (2005). https:\/\/doi.org\/10.1145\/1047659.1040317","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. Int. J. Softw. Tools Technol. Transfer (2), 185\u2013204 (2004). https:\/\/doi.org\/10.1007\/s10009-003-0121-x","DOI":"10.1007\/s10009-003-0121-x"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Sindoni, G., Griggio, A., Tonetta, S.: Certifying rLive: a new proof strategy for liveness model checking. In: Thiemann, R., Weidenbach, C. (eds.) Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings. Lecture Notes in Computer Science, vol. 15979, pp. 386\u2013403. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-032-04167-8_21","DOI":"10.1007\/978-3-032-04167-8_21"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Sindoni, G., Pasini, P., Cabodi, G.: A theorem prover based approach for SAT-based model checking. In: Automated Deduction-CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, 28\u201331 July 2025, Proceedings. vol. 15943, p. 449. Springer Nature (2025). https:\/\/doi.org\/10.1007\/978-3-031-99984-0_24","DOI":"10.1007\/978-3-031-99984-0_24"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Sprenger, C.: A verified model checker for the modal $$\\upmu $$-calculus in Coq. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 167\u2013183. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0054171","DOI":"10.1007\/BFb0054171"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"Urban, C.: FuncTion: an abstract domain functor for termination: (competition contribution). In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 464\u2013466. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_46","DOI":"10.1007\/978-3-662-46681-0_46"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: 24th Annual Symposium on Foundations of Computer Science (SFCS 1983), pp. 185\u2013194. IEEE (1983). https:\/\/doi.org\/10.1006\/inco.1994.1092","DOI":"10.1006\/inco.1994.1092"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"Xia, Y., Cimatti, A., Griggio, A., Li, J.: Avoiding the shoals - a new approach to liveness checking. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, 24\u201327 July 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 234\u2013254. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_12","DOI":"10.1007\/978-3-031-65627-9_12"},{"key":"1_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-030-81688-9_17","volume-title":"Computer Aided Verification","author":"E Yu","year":"2021","unstructured":"Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 363\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_17"},{"key":"1_CR48","doi-asserted-by":"publisher","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Towards compositional hardware model checking certification. In: Nadel, A., Rozier, K.Y. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, 24\u201327 October 2023, pp. 1\u201311. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_12","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_12"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32537-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:41:47Z","timestamp":1784796107000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32537-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325365","9783032325372"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32537-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}