{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T12:27:40Z","timestamp":1746793660537},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_33","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T17:40:06Z","timestamp":1289238006000},"page":"501-517","source":"Crossref","is-referenced-by-count":7,"title":["A Combination of Forward and Backward Reachability Analysis Methods"],"prefix":"10.1007","author":[{"given":"Kazuhiro","family":"Ogata","sequence":"first","affiliation":[]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","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, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"33_CR2","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A lightweight object modeling notation. ACM TOSEM\u00a011, 256\u2013290 (2002)","journal-title":"ACM TOSEM"},{"key":"33_CR3","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S. Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyser and its meta-logical properties. TCS\u00a0367, 162\u2013202 (2006)","journal-title":"TCS"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11901433_7","volume-title":"Formal Methods and Software Engineering","author":"K. Ogata","year":"2006","unstructured":"Ogata, K., Nakano, M., Kong, W., Futatsugi, K.: Induction-guided falsification. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 114\u2013131. Springer, Heidelberg (2006)"},{"key":"33_CR5","series-title":"AMAST Series in Computing","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume-title":"CafeOBJ report","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing, vol.\u00a06. World Scientific, Singapore (1998)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude \u2013 A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"33_CR7","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. CACM\u00a021, 993\u2013999 (1978)","journal-title":"CACM"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"33_CR9","unstructured":"Denker, G., Meseguer, J., Talcott, C.: Protocol specification and analysis in Maude. In: Workshop on Formal Methods and Security Protocols (1998)"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/11780274_31","volume-title":"Algebra, Meaning, and Computation","author":"K. Ogata","year":"2006","unstructured":"Ogata, K., Futatsugi, K.: Some tips on writing proof scores in the OTS\/CafeOBJ method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol.\u00a04060, pp. 596\u2013615. Springer, Heidelberg (2006)"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-03741-2_27","volume-title":"Algebra and Coalgebra in Computer Science","author":"D. G\u00e2in\u00e2","year":"2009","unstructured":"G\u00e2in\u00e2, D., Futatsugi, K., Ogata, K.: Constructor-based institutions. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 398\u2013412. Springer, Heidelberg (2009)"},{"key":"33_CR12","first-page":"198","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE TIT\u00a0IT-29, 198\u2013208 (1983)","journal-title":"IEEE TIT"},{"key":"33_CR13","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. IPL\u00a056, 131\u2013133 (1995)","journal-title":"IPL"},{"key":"33_CR14","series-title":"LNCS","first-page":"14","volume-title":"15th CAV","author":"L. Moura de","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: CAV 2003. LNCS, vol.\u00a02392, pp. 14\u201326. Springer, Heidelberg (2003)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"33_CR16","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"678","DOI":"10.1007\/978-3-642-16901-4_44","volume-title":"12th ICFEM","author":"M. Zhang","year":"2010","unstructured":"Zhang, M., Ogata, K., Nakamura, M.: Specification translation of state machines from equational theories into rewrite theories. In: Zhu, H. (ed.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 678\u2013693. Springer, Heidelberg (2010)"},{"key":"33_CR18","first-page":"783","volume":"17","author":"M. Nakano","year":"2007","unstructured":"Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Cr\u00e8me: An automatic invariant prover of behavioral specifications. IJSEKE\u00a017, 783\u2013804 (2007)","journal-title":"IJSEKE"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T04:10:40Z","timestamp":1553227840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}