{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,19]],"date-time":"2025-11-19T06:54:08Z","timestamp":1763535248151},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319030760"},{"type":"electronic","value":"9783319030777"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03077-7_3","type":"book-chapter","created":{"date-parts":[[2013,10,28]],"date-time":"2013-10-28T01:40:21Z","timestamp":1382924421000},"page":"32-43","source":"Crossref","is-referenced-by-count":10,"title":["Increasing Confidence in Liveness Model Checking Results with Proofs"],"prefix":"10.1007","author":[{"given":"Tuomas","family":"Kuismin","sequence":"first","affiliation":[]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"AIGER: A format, library and set of utilities for And-Inverter Graphs (AIGs), \n                    \n                      http:\/\/fmv.jku.at\/aiger\/"},{"key":"3_CR2","unstructured":"The IImc model checker, \n                    \n                      http:\/\/ecee.colorado.edu\/~bradleya\/iimc\/"},{"key":"3_CR3","unstructured":"The Racket programming language, \n                    \n                      http:\/\/racket-lang.org\/"},{"key":"3_CR4","unstructured":"Balint, A., Belov, A., Heule, M., J\u00e4rvisalo, M.: The international SAT competition, \n                    \n                      http:\/\/satcompetition.org\/"},{"issue":"2","key":"3_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.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci.\u00a066(2), 160\u2013177 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) TACAS. Lecture Notes in Computer Science, vol. 1579, pp. 193\u2013207. Springer (1999)"},{"key":"3_CR7","unstructured":"Biere, A., Heljanko, K., Seidl, M., Wieringa, S.: Hardware model checking competition 2012 (2012), \n                    \n                      http:\/\/fmv.jku.at\/hwmcc12\/"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","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":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D.A. (eds.) VMCAI. Lecture Notes in Computer Science, vol. 6538, pp. 70\u201387. Springer (2011)"},{"key":"3_CR9","unstructured":"Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: Bjesse, P., Slobodov\u00e1, A. (eds.) FMCAD. pp. 144\u2013153. FMCAD Inc. (2011)"},{"issue":"2","key":"3_CR10","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput.\u00a098(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"3_CR11","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: Cabodi, G., Singh, S. (eds.) FMCAD, pp. 52\u201359. IEEE (2012)"},{"issue":"4","key":"3_CR12","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci.\u00a089(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable ltl model checker. In: Sharygina, N., Veith, H. (eds.) CAV. Lecture Notes in Computer Science, vol. 8044, pp. 463\u2013478. Springer (2013)"},{"key":"3_CR14","unstructured":"E\u00e9n, N.: The ABC\/ZZ verification and synthesis framework, \n                    \n                      https:\/\/bitbucket.org\/niklaseen\/abc-zz"},{"key":"3_CR15","unstructured":"Gan, X., Dubrovin, J., Heljanko, K.: A symbolic model checking approach to verifying satellite onboard software. Science of Computer Programming (2013), \n                    \n                      http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642313000658"},{"key":"3_CR16","unstructured":"Kuismin, T.: Liveness to safety reduction, implementation, \n                    \n                      http:\/\/users.ics.aalto.fi\/tlauniai\/live2safe\/"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.ress.2012.03.021","volume":"105","author":"J. Lahtinen","year":"2012","unstructured":"Lahtinen, J., Valkonen, J., Bj\u00f6rkman, K., Frits, J., Niemel\u00e4, I., Heljanko, K.: Model checking of safety-critical software in the nuclear engineering domain. Rel. Eng. & Sys. Safety\u00a0105, 104\u2013113 (2012)","journal-title":"Rel. Eng. & Sys. Safety"},{"key":"3_CR18","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":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 2\u201313. Springer, Heidelberg (2001)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Ray, S., Hunt Jr., W.A.: Mechanized certification of secure hardware designs. In: Abadir, M.S., Wang, L.C., Bhadra, J. (eds.) MTV, pp. 25\u201332. IEEE Computer Society (2007)","DOI":"10.1109\/MTV.2007.16"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0054171","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Sprenger","year":"1998","unstructured":"Sprenger, C.: A verified model checker for the modal \u03bc-calculus in Coq. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 167\u2013183. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03077-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T00:15:22Z","timestamp":1558656922000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03077-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319030760","9783319030777"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03077-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}