{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:53:40Z","timestamp":1743022420587,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66197-1_4","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"54-69","source":"Crossref","is-referenced-by-count":14,"title":["From Model Checking to a Temporal Proof for Partial Models"],"prefix":"10.1007","author":[{"given":"Anna","family":"Bernasconi","sequence":"first","affiliation":[]},{"given":"Claudio","family":"Menghi","sequence":"additional","affiliation":[]},{"given":"Paola","family":"Spoletini","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]},{"given":"Carlo","family":"Ghezzi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"key":"4_CR1","unstructured":"Alavi, H., Avrunin, G., Corbett, J., Dillon, L., Dwyer, M., Pasareanu, C.: Spec patterns (2017). \nhttp:\/\/patterns.projects.cs.ksu.edu\/documentation\/patterns\/ltl.shtml"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.entcs.2006.04.004","volume":"158","author":"A Antonik","year":"2006","unstructured":"Antonik, A., Huth, M.: Efficient patterns for model checking partial state spaces in CTL $$\\cap $$ LTL. Electron. Notes Theor. Comput. Sci. 158, 41\u201357 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: Formal Methods and Models for Codesign, pp. 80\u201389. IEEE (2015)","DOI":"10.1109\/MEMCOD.2015.7340473"},{"key":"4_CR4","unstructured":"Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L., Ghezzi, C.: From model checking to a temporal proof for partial models: preliminary example (2017). arXiv preprint \narXiv:1706.02701"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999). doi:\n10.1007\/3-540-48683-6_25"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"G Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168\u2013182. Springer, Heidelberg (2000). doi:\n10.1007\/3-540-44618-4_14"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-27836-8_26","volume-title":"Automata, Languages and Programming","author":"G Bruns","year":"2004","unstructured":"Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281\u2013293. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-27836-8_26"},{"key":"4_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7\u201315. ACM (1998)","DOI":"10.1145\/298595.298598"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Protocol Specification, Testing and Verification","author":"R Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembi\u0144ski, P., \u015aredniawa, M. (eds.) Protocol Specification, Testing and Verification, pp. 3\u201318. Springer, Boston (1996). doi:\n10.1007\/978-0-387-34892-6_1"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Huth, M.: Model checking vs. generalized model checking: semantic minimizations for temporal logics. In: Logic in Computer Science, pp. 158\u2013167. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.28"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 \u2014 Concurrency Theory","author":"P Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426\u2013440. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-44685-0_29"},{"issue":"6","key":"4_CR13","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/s10009-010-0169-3","volume":"13","author":"P Godefroid","year":"2011","unstructured":"Godefroid, P., Piterman, N.: LTL generalized model checking revisited. Int. J. Softw. Tools Technol. Transfer 13(6), 571\u2013584 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). doi:\n10.1007\/3-540-63166-6_10"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-45187-7_18","volume-title":"CONCUR 2003 - Concurrency Theory","author":"A Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Multi-valued model checking via classical model checking. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 266\u2013280. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-45187-7_18"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11560548_8","volume-title":"Correct Hardware Design and Verification Methods","author":"A Gurfinkel","year":"2005","unstructured":"Gurfinkel, A., Chechik, M.: How thorough is thorough enough? In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 65\u201380. Springer, Heidelberg (2005). doi:\n10.1007\/11560548_8"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Logic in Computer Science, pp. 203\u2013210. IEEE (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"4_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-48989-6_32","volume-title":"FM 2016: Formal Methods","author":"C Menghi","year":"2016","unstructured":"Menghi, C., Spoletini, P., Ghezzi, C.: Dealing with incompleteness in automata-based model checking. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 531\u2013550. Springer, Cham (2016). doi:\n10.1007\/978-3-319-48989-6_32"},{"key":"4_CR20","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). doi:\n10.1007\/3-540-44585-4_2"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-45294-X_25","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"D Peled","year":"2001","unstructured":"Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292\u2013304. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-45294-X_25"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45139-0_1","volume-title":"Model Checking Software","author":"D Peled","year":"2001","unstructured":"Peled, D., Zuck, L.: From model checking to a temporal proof. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 1\u201314. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-45139-0_1"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer Aided Verification","author":"S Rajan","year":"1995","unstructured":"Rajan, S., Shankar, N., Srivas, M.K.: An integration of model checking with automated proof checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 84\u201397. Springer, Heidelberg (1995). doi:\n10.1007\/3-540-60045-0_42"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-45657-0_37","volume-title":"Computer Aided Verification","author":"L Tan","year":"2002","unstructured":"Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455\u2013470. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45657-0_37"},{"issue":"4","key":"4_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"Jim Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4) (2009)","journal-title":"ACM Computing Surveys"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,24]],"date-time":"2018-07-24T23:45:35Z","timestamp":1532475935000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}