{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:08Z","timestamp":1779087608660,"version":"3.51.4"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T00:00:00Z","timestamp":1624492800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T00:00:00Z","timestamp":1624492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s10703-021-00369-1","type":"journal-article","created":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T08:03:12Z","timestamp":1624521792000},"page":"178-210","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Certifying proofs for SAT-based model checking"],"prefix":"10.1007","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9483-3940","authenticated-orcid":false,"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,24]]},"reference":[{"key":"369_CR1","unstructured":"Barrett C, Fontaine P, Tinelli C (2017) The SMT-LIB standard: version 2.6. Tech. rep., Department of Computer Science, The University of Iowa. www.SMT-LIB.org"},{"key":"369_CR2","doi-asserted-by":"crossref","unstructured":"Basin D, Bhatt BN, Traytel D (2018) Optimal proofs for linear temporal logic on lasso words . https:\/\/www21.in.tum.de\/~traytel\/papers\/expl\/expl.pdf","DOI":"10.1007\/978-3-030-01090-4_3"},{"key":"369_CR3","unstructured":"Ben-Ari M (1993) Mathematical logic for computer science. Prentice Hall International series in computer science. Prentice Hall"},{"key":"369_CR4","doi-asserted-by":"crossref","unstructured":"Bernasconi A, Menghi C, Spoletini P, Zuck LD, Ghezzi C (2017) From model checking to a temporal proof for partial models. In: SEFM, LNCS, vol. 10469, pp 54\u201369. Springer","DOI":"10.1007\/978-3-319-66197-1_4"},{"issue":"2","key":"369_CR5","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 (2002) Liveness checking as safety checking. Electr Notes Theor Comput Sci 66(2):160\u2013177. https:\/\/doi.org\/10.1016\/S1571-0661(04)80410-9","journal-title":"Electr Notes Theor Comput Sci"},{"key":"369_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:117\u2013148. https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2(03)58003-2","journal-title":"Adv Comput"},{"key":"369_CR7","doi-asserted-by":"crossref","unstructured":"Biere A, van Dijk T, Heljanko K (2017) Hardware model checking competition 2017. In: Proceedings of the 17th conference on formal methods in computer-aided design, FMCAD \u201917, pp 9. FMCAD Inc, Austin, TX . http:\/\/dl.acm.org\/citation.cfm?id=3168451.3168458","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"369_CR8","unstructured":"Biere A, Heljanko K, Wieringa S (2011) AIGER 1.9 and beyond. Tech. rep., FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria"},{"key":"369_CR9","unstructured":"Bjesse P, Kukula JH (2005) Automatic generalized phase abstraction for formal verification. In: ICCAD, pp 1076\u20131082. IEEE Computer Society"},{"key":"369_CR10","doi-asserted-by":"crossref","unstructured":"Bozzano M, Cimatti A, Pires AF, Jones D, Kimberly G, Petri T, Robinson R, Tonetta S (2015) Formal design and safety analysis of AIR6110 wheel brake system. In: CAV (1), LNCS, vol 9206, pp 518\u2013535. Springer","DOI":"10.1007\/978-3-319-21690-4_36"},{"key":"369_CR11","doi-asserted-by":"crossref","unstructured":"Bradley A (2011) SAT-based model checking without unrolling. In: VMCAI, LNCS, vol 6538, pp 70\u201387. Springer","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"369_CR12","unstructured":"Bradley AR, Somenzi F, Hassan Z, Zhang Y (2011) An incremental approach to model checking progress properties. In: FMCAD, pp 144\u2013153. FMCAD Inc"},{"key":"369_CR13","unstructured":"Case ML, Baumgartner J, Mony H, Kanzelman R (2011).Optimal redundancy removal without fixedpoint computation. In: Bjesse P, Slobodov\u00e1 A (eds) international conference on formal methods in computer-aided design, FMCAD \u201911, Austin, TX, USA, October 30\u2013November 02, 2011, pp 101\u2013108. FMCAD Inc. http:\/\/dl.acm.org\/citation.cfm?id=2157672"},{"key":"369_CR14","doi-asserted-by":"crossref","unstructured":"Case ML, Mony H, Baumgartner J, Kanzelman R (2009) Enhanced verification by temporal decomposition. In: FMCAD. IEEE","DOI":"10.1109\/FMCAD.2009.5351146"},{"key":"369_CR15","doi-asserted-by":"crossref","unstructured":"Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In: CAV, LNCS, vol 8559, pp 334\u2013342. Springer","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"369_CR16","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: TACAS, LNCS, vol 7795. Springer","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"369_CR17","doi-asserted-by":"crossref","unstructured":"Cini C, Francalanza A (2015) An LTL proof system for runtime verification. In: TACAS, LNCS, vol 9035, pp 581\u2013595. Springer","DOI":"10.1007\/978-3-662-46681-0_54"},{"key":"369_CR18","unstructured":"Claessen K, S\u00f6rensson N (2012) A liveness checking algorithm that counts. In: Cabodi G, Singh S (eds) FMCAD, pp 52\u201359. IEEE"},{"issue":"1","key":"369_CR19","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"EM Clarke","year":"1997","unstructured":"Clarke EM, Grumberg O, Hamaguchi K (1997) Another look at LTL model checking. Formal Methods Syst Des 10(1):47\u201371","journal-title":"Formal Methods Syst Des"},{"key":"369_CR20","doi-asserted-by":"crossref","unstructured":"Daniel J, Cimatti A, Griggio A, Tonetta S, Mover S (2016) Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In: CAV (1), LNCS, vol 9779. Springer","DOI":"10.1007\/978-3-319-41528-4_15"},{"key":"369_CR21","doi-asserted-by":"crossref","unstructured":"Dax C, Hofmann M, Lange M (2006) A proof system for the linear time $$\\rm \\mu $$-calculus. In: FSTTCS, LNCS, vol 4337, pp 273\u2013284. Springer","DOI":"10.1007\/11944836_26"},{"key":"369_CR22","doi-asserted-by":"publisher","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible sat-solver. In: Giunchiglia E, Tacchella A (eds) Theory and applications of satisfiability testing, 6th international conference, SAT 2003. Santa Margherita Ligure, Italy, May 5\u20138, 2003 Selected Revised Papers, Lecture Notes in Computer Science, vol 2919, pp 502\u2013518. Springer . https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"1\u20132","key":"369_CR23","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1016\/S0304-3975(00)00034-7","volume":"258","author":"EA Emerson","year":"2001","unstructured":"Emerson EA, Jutla CS, Sistla AP (2001) On model checking for the $$\\rm \\mu $$-calculus and its fragments. Theor Comput Sci 258(1\u20132):491\u2013522. https:\/\/doi.org\/10.1016\/S0304-3975(00)00034-7","journal-title":"Theor Comput Sci"},{"key":"369_CR24","doi-asserted-by":"crossref","unstructured":"Esparza J, Lammich P, Neumann R, Nipkow T, Schimpf A, Smaus J (2014) A fully verified executable LTL model checker. Arch Formal Proofs 2014","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"369_CR25","doi-asserted-by":"crossref","unstructured":"Fisler K, Kurshan RP (1997) Verifying VHDL designs with COSPAN. In: FHV, LNCS, vol 1287, pp 206\u2013247. Springer","DOI":"10.1007\/3-540-63475-4_5"},{"key":"369_CR26","doi-asserted-by":"publisher","unstructured":"Gabbay DM, Pnueli A, Shelah S, Stavi J (1980) On the temporal basis of fairness. In: Conference record of the seventh annual ACM symposium on principles of programming languages, Las Vegas, Nevada, USA, January 1980, pp 163\u2013173 . https:\/\/doi.org\/10.1145\/567446.567462","DOI":"10.1145\/567446.567462"},{"key":"369_CR27","doi-asserted-by":"publisher","unstructured":"Griggio A, Roveri M (2016) Comparing different variants of the ic3 algorithm for hardware model checking. IEEE Trans CAD Integrated Circuits Syst 35(6), 1026\u20131039 . https:\/\/doi.org\/10.1109\/TCAD.2015.2481869","DOI":"10.1109\/TCAD.2015.2481869"},{"key":"369_CR28","doi-asserted-by":"publisher","unstructured":"Griggio A, Roveri M, Tonetta S (2018) Certifying proofs for LTL model checking. In: 2018 formal methods in computer aided design, FMCAD 2018, Austin, TX, USA, October 30\u2013November 2, 2018, pp 1\u20139. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603022","DOI":"10.23919\/FMCAD.2018.8603022"},{"key":"369_CR29","doi-asserted-by":"crossref","unstructured":"Hustadt U, Konev B (2003) TRP++2.0: a temporal resolution prover. In: CADE-19, LNCS, vol 2741. Springer","DOI":"10.1007\/978-3-540-45085-6_21"},{"key":"369_CR30","doi-asserted-by":"crossref","unstructured":"Hustadt U, Konev B, Riazanov A, Voronkov A (2004) Temp: a temporal monodic prover. In: IJCAR, LNCS, vol 3097. Springer","DOI":"10.1007\/978-3-540-25984-8_23"},{"key":"369_CR31","doi-asserted-by":"publisher","unstructured":"Kuismin T, Heljanko K (2013) Increasing confidence in liveness model checking results with proofs. In: Bertacco V, Legay A (eds) Hardware and software: verification and testing - 9th international haifa verification conference, HVC 2013, Haifa, Israel, November 5\u20137, 2013, Proceedings, Lecture Notes in Computer Science, vol 8244, pp 32\u201343. Springer. https:\/\/doi.org\/10.1007\/978-3-319-03077-7_3","DOI":"10.1007\/978-3-319-03077-7_3"},{"issue":"1","key":"369_CR32","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.tcs.2005.07.021","volume":"345","author":"O Kupferman","year":"2005","unstructured":"Kupferman O, Vardi MY (2005) From complementation to certification. Theor Comput Sci 345(1):83\u2013100. https:\/\/doi.org\/10.1016\/j.tcs.2005.07.021","journal-title":"Theor Comput Sci"},{"key":"369_CR33","doi-asserted-by":"publisher","unstructured":"Mebsout A, Tinelli C (2016) Proof certificates for SMT-based model checkers for infinite-state systems. In: 2016 formal methods in computer-aided design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016, pp 117\u2013124 . https:\/\/doi.org\/10.1109\/FMCAD.2016.7886669","DOI":"10.1109\/FMCAD.2016.7886669"},{"key":"369_CR34","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Proofs and refutations, and Z3. In: LPAR workshops, CEUR workshop proceedings, vol 418. CEUR-WS.org"},{"key":"369_CR35","doi-asserted-by":"crossref","unstructured":"Namjoshi KS (2001) Certifying model checkers. In: CAV, LNCS, vol 2102. Springer","DOI":"10.1007\/3-540-44585-4_2"},{"key":"369_CR36","doi-asserted-by":"crossref","unstructured":"Peled DA, Pnueli A, Zuck LD (2001) From falsification to verification. In: Hariharan R, Mukund M, Vinay V (eds.) FST TCS 2001, LNCS, vol 2245, pp 292\u2013304. Springer","DOI":"10.1007\/3-540-45294-X_25"},{"key":"369_CR37","doi-asserted-by":"crossref","unstructured":"Peled DA, Zuck LD (2001) From model checking to a temporal proof. In: SPIN, LNCS, vol 2057. Springer","DOI":"10.1007\/3-540-45139-0_1"},{"key":"369_CR38","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: FOCS, pp 46\u201357. 10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"369_CR39","volume-title":"Natural deduction: a proof-theoretical study","author":"D Prawitz","year":"2006","unstructured":"Prawitz D (2006) Natural deduction: a proof-theoretical study. Dover Books on Mathematics, Dover Publications"},{"key":"369_CR40","unstructured":"RTCA DO-333: Formal Methods Supplement to DO-178C and DO-278A (2011)"},{"key":"369_CR41","doi-asserted-by":"crossref","unstructured":"Schuppan V, Darmawan L (2011) Evaluating LTL satisfiability solvers. In: ATVA, LNCS, vol 6996. Springer","DOI":"10.1007\/978-3-642-24372-1_28"},{"issue":"2","key":"369_CR42","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"CH Seger","year":"1995","unstructured":"Seger CH, Bryant RE (1995) Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods Syst Des 6(2):147\u2013189. https:\/\/doi.org\/10.1007\/BF01383966","journal-title":"Formal Methods Syst Des"},{"key":"369_CR43","doi-asserted-by":"crossref","unstructured":"Vardi MY (1995) An automata-theoretic approach to linear temporal logic. In: Banff Higher Order Workshop, LNCS, vol 1043, pp 238\u2013266. Springer","DOI":"10.1007\/3-540-60915-6_6"},{"key":"369_CR44","doi-asserted-by":"publisher","unstructured":"Wagner LG, Mebsout A, Tinelli C, Cofer DD, Slind K (2017) qualification of a model checker for avionics software verification. In: NASA formal methods - 9th international symposium, NFM 2017, Moffett Field, CA, USA, May 16\u201318, 2017, Proceedings, pp 404\u2013419 . https:\/\/doi.org\/10.1007\/978-3-319-57288-8_29","DOI":"10.1007\/978-3-319-57288-8_29"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00369-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00369-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00369-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T18:11:54Z","timestamp":1636481514000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00369-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,24]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["369"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00369-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,24]]},"assertion":[{"value":"19 March 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}