{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:13:59Z","timestamp":1758053639184,"version":"3.44.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"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>SAT-based model checking has become a prominent approach to\u00a0the verification of temporal properties. However, while invariant\u00a0model checking can produce simple proofs based on induction,\u00a0proof generation for SAT-based model checking of liveness properties is\u00a0much more complex.<\/jats:p>\n          <jats:p>In this paper, we focus on a recently developed algorithm, called rlive, which has been proved quite effective in practice. rlive\u00a0tries to find a counterexample with a series of reachability checks,\u00a0while iteratively blocking shoals, i.e., set of states that cannot\u00a0be extended with fair paths. Despite the complexity of the algorithm,\u00a0we show that the shoals are sufficient to generate a proof in a deductive system for temporal properties. We implement the approach in\u00a0an existing certifying model checking framework based on the PVS theorem prover, and we experimentally evaluate it on liveness verification problems from the hardware model checking competition, generating proofs using the nuXmv model checker and checking them with PVS.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_21","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:18Z","timestamp":1757887458000},"page":"386-403","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Certifying rlive: A New Proof Strategy for\u00a0Liveness Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4003-2317","authenticated-orcid":false,"given":"Giulia","family":"Sindoni","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"issue":"2","key":"21_CR1","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electron. Notes Theor. Comput. Sci. 66(2), 160\u2013177 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR2","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical Report 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"21_CR3","unstructured":"Biere, A., Jussila, T.: The Model Checking Competition Web Page, http:\/\/fmv.jku.at\/hwmcc"},{"key":"21_CR4","unstructured":"Biere, A., Yu, E., Froleyks, N.: Stratified certification for k-induction. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design\u2013FMCAD 2022, vol. 3, p. 59. TU Wien Academic Press (2022)"},{"key":"21_CR5","unstructured":"Boulton, R.J., et al.: Experience with embedding hardware description languages in HOL. In: TPCD, vol. 10, pp. 129\u2013156 (1992)"},{"key":"21_CR6","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)"},{"key":"21_CR7","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuXmv Symbolic Model Checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Johannsen, C., Rozier, K.Y., Tonetta, S.: Infinite state liveness checking with rlive. In: Proceedings of the 37th International Conference on Computer Aided Verification (CAV 2025) (2025). To be published","DOI":"10.1007\/978-3-031-98668-0_11"},{"key":"21_CR9","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)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Dax, C., Hofmann, M., Lange. M.: A proof system for the linear time $$\\mu $$-calculus. In: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science: 26th International Conference, Kolkata, India, December 13-15, 2006. Proceedings 26, pp. 273\u2013284. Springer (2006)","DOI":"10.1007\/11944836_26"},{"key":"21_CR11","unstructured":"Dutertre, B., De Moura, L.: The yices smt solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper. pdf, 2(2), 1\u20132 (2006)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Froleyks, N., Yu, E., Biere, A., Heljanko, K.: Certifying phase abstraction. In: International Joint Conference on Automated Reasoning, pp. 284\u2013303. Springer (2024)","DOI":"10.1007\/978-3-031-63498-7_17"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 163\u2013173 (1980)","DOI":"10.1145\/567446.567462"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische schlie\u00dfen. i. Mathematische zeitschrift, 35 (1935)","DOI":"10.1007\/BF01201363"},{"issue":"2","key":"21_CR15","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. Des. 57(2), 178\u2013210 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Kuismin, T., Heljanko, K.: Increasing confidence in liveness model checking results with proofs. In: Haifa Verification Conference, pp. 32\u201343. Springer (2013)","DOI":"10.1007\/978-3-319-03077-7_3"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: From complementation to certification. Theor. Comput. Sci. 345(1), 83\u2013100 (2005)","DOI":"10.1016\/j.tcs.2005.07.021"},{"key":"21_CR18","unstructured":"Munoz, C.A.: Batch proving and proof scripting in PVS. Technical report, National Institute of Aerospace (2007)"},{"key":"21_CR19","doi-asserted-by":"publisher","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","DOI":"10.1007\/3-540-44585-4_2"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction, pp. 748\u2013752. Springer, 1992","DOI":"10.1007\/3-540-55602-8_217"},{"key":"21_CR21","unstructured":"Owre, S., Shankar, N.: Writing PVS proof strategies. In: Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), number CP-2003-212448 in NASA Conference Publication, pp. 1\u201315 (2003)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: International Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 292\u2013304. Springer (2001)","DOI":"10.1007\/3-540-45294-X_25"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Peled, D., Zuck, L.: From model checking to a temporal proof. In: International SPIN workshop on model checking of software, pp. 1\u201314. Springer (2001)","DOI":"10.1007\/3-540-45139-0_1"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium On Foundations of Computer Science (sfcs 1977), pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"21_CR25","unstructured":"Rushby, J.: PVS embeddings of propositional and quantified modal logic. arXiv preprint arXiv:2205.06391 (2022)"},{"key":"21_CR26","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS prover guide. Comput. Sci. Lab. SRI Int. Menlo Park, CA 1, 11\u201312 (2001)"},{"key":"21_CR27","unstructured":"Sindoni, G., Griggio, A., Tonetta, S.: Certifying-rlive-25. https:\/\/gitlab.fbk.eu\/gsindoni\/Certifying_Rlive_25. Accessed 15 May 2025"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Sindoni, G., et al.: Giulia Sindoni, et al.: A theorem prover based approach for sat-based model checking certification. In: Automated Deduction-CADE- 35: 30th International Conference on Automated Deduction, Stuttgart, Germany, 2025, Proceedings 30 (2025). To be published","DOI":"10.1007\/978-3-031-99984-0_24"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for concurrency: structure versus automata, pp. 238\u2013266 (2005)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Xia, Y., Cimatti, A., Griggio, A., Li, J.: Avoiding the shoals-a new approach to liveness checking. In: International Conference on Computer Aided Verification, pp. 234\u2013254. Springer (2024)","DOI":"10.1007\/978-3-031-65627-9_12"},{"key":"21_CR31","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-030-81688-9_17"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:24Z","timestamp":1757887464000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","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":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}