{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:28:35Z","timestamp":1747888115613,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466803"},{"type":"electronic","value":"9783662466810"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_58","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T22:56:36Z","timestamp":1427756196000},"page":"643-657","source":"Crossref","is-referenced-by-count":4,"title":["Saturation-Based Incremental LTL Model Checking with Inductive Proofs"],"prefix":"10.1007","author":[{"given":"Vince","family":"Moln\u00e1r","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D\u00e1niel","family":"Darvas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tam\u00e1s","family":"Bartha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"58_CR1","doi-asserted-by":"crossref","unstructured":"Biere, A., Zhu, Y., Clarke, E.: Multiple state and single state tableaux for combining local and global model checking. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol.\u00a01710, pp. 163\u2013179. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48092-7_8"},{"key":"58_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31612-8_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Bradley","year":"2012","unstructured":"Bradley, A.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 1\u201314. Springer, Heidelberg (2012)"},{"key":"58_CR3","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Mariotti, A., Micheli, A., Mover, S., Griggio, A., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. Tech. rep., Fondazione Bruno Kessler (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"58_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ciardo","year":"2001","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 328\u2013342. Springer, Heidelberg (2001)"},{"issue":"1","key":"58_CR5","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. Int. J. on Softw. Tools for Technology Transfer\u00a08(1), 4\u201325 (2006)","journal-title":"Int. J. on Softw. Tools for Technology Transfer"},{"key":"58_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., et al.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"58_CR7","unstructured":"Claessen, K., Sorensson, N.: A liveness checking algorithm that counts. In: Formal Methods in Computer-Aided Design, 2012, pp. 52\u201359. IEEE (2012)"},{"key":"58_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BFb0023737","volume-title":"Computer-Aided Verification","author":"C. Courcoubetis","year":"1991","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 233\u2013242. Springer, Heidelberg (1991)"},{"key":"58_CR9","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using transition-based generalized B\u00fcchi automata. In: Proc. of the IEEE Int. Symp. on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, pp. 76\u201383 (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"58_CR10","unstructured":"Duret-Lutz, A., Klai, K., Poitrenaud, D., Thierry-Mieg, Y.: Combining explicit and symbolic approaches for better on-the-fly LTL model checking. arXiv:1106.5700 (cs) (2011)"},{"key":"58_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-30476-0_19","volume-title":"Automated Technology for Verification and Analysis","author":"S. Haddad","year":"2004","unstructured":"Haddad, S., Ili\u00e9, J.M., Klai, K.: Design and evaluation of a symbolic and abstraction-based model checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 196\u2013210. Springer, Heidelberg (2004)"},{"key":"58_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-68746-7_20","volume-title":"Applications and Theory of Petri Nets","author":"K. Klai","year":"2008","unstructured":"Klai, K., Poitrenaud, D.: MC-SOG: An LTL model checker based on symbolic observation graphs. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol.\u00a05062, pp. 288\u2013306. Springer, Heidelberg (2008)"},{"key":"58_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/11513988_35","volume-title":"Computer Aided Verification","author":"R. Sebastiani","year":"2005","unstructured":"Sebastiani, R., Tonetta, S., Vardi, M.: Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 350\u2013363. Springer, Heidelberg (2005)"},{"key":"58_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/3-540-36126-X_6","volume-title":"Formal Methods in Computer-Aided Design","author":"F. Somenzi","year":"2002","unstructured":"Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic SCC hull algorithms. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 88\u2013105. Springer, Heidelberg (2002)"},{"issue":"2","key":"58_CR15","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth first search and linear graph algorithms. SIAM Journal on Computing\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM Journal on Computing"},{"issue":"1","key":"58_CR16","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-006-4617-3","volume":"28","author":"C. Wang","year":"2006","unstructured":"Wang, C., Bloem, R., Hachtel, G.D., Ravi, K., Somenzi, F.: Compositional SCC analysis for language emptiness. Form. Method. Syst. Des.\u00a028(1), 5\u201336 (2006)","journal-title":"Form. Method. Syst. Des."},{"key":"58_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-04761-9_27","volume-title":"Automated Technology for Verification and Analysis","author":"Y. Zhao","year":"2009","unstructured":"Zhao, Y., Ciardo, G.: Symbolic CTL model checking of asynchronous systems using constrained saturation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 368\u2013381. Springer, Heidelberg (2009)"},{"issue":"2","key":"58_CR18","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s11334-011-0146-3","volume":"7","author":"Y. Zhao","year":"2011","unstructured":"Zhao, Y., Ciardo, G.: Symbolic computation of strongly connected components and fair cycles using saturation. Innov. Syst. Softw. Eng.\u00a07(2), 141\u2013150 (2011)","journal-title":"Innov. Syst. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_58","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:25:29Z","timestamp":1747855529000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}