{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:05:20Z","timestamp":1725473120843},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540474609"},{"type":"electronic","value":"9783540474623"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11901433_7","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"114-131","source":"Crossref","is-referenced-by-count":9,"title":["Induction-Guided Falsification"],"prefix":"10.1007","author":[{"given":"Kazuhiro","family":"Ogata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masahiro","family":"Nakano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weiqiang","family":"Kong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-39958-2_12","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 170\u2013184. Springer, Heidelberg (2003)"},{"key":"7_CR2","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":"7_CR3","first-page":"357","volume-title":"2nd APAQS","author":"K. Ogata","year":"2001","unstructured":"Ogata, K., Futatsugi, K.: Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm. In: 2nd APAQS, pp. 357\u2013366. IEEE CS Press, Los Alamitos (2001)"},{"key":"7_CR4","first-page":"181","volume-title":"5th FMOODS","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm. In: 5th FMOODS, pp. 181\u2013195. Kluwer, Dordrecht (2002)"},{"key":"7_CR5","series-title":"ENTCS 71","volume-title":"4th WRLA 2002","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: 4th WRLA 2002. ENTCS 71. Elsevier, Amsterdam (2002)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-36532-X_25","volume-title":"Software Security \u2013 Theories and Systems","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of the iKP electronic payment protocols. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 441\u2013460. Springer, Heidelberg (2003)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-36384-X_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Formal verification of the Horn-Preneel micropayment protocol. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 238\u2013252. Springer, Heidelberg (2002)"},{"key":"7_CR8","first-page":"50","volume-title":"4th QSIC","author":"K. Ogata","year":"2004","unstructured":"Ogata, K., Futatsugi, K.: Equational approach to formal verification of SET. In: 4th QSIC, pp. 50\u201359. IEEE CS Press, Los Alamitos (2004)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-540-37621-7_3","volume-title":"Software Security - Theories and Systems","author":"K. Ogata","year":"2004","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of the NetBill electronic commerce protocol. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol.\u00a03233, pp. 45\u201364. Springer, Heidelberg (2004)"},{"key":"7_CR10","first-page":"795","volume-title":"25th ICDCS","author":"K. Ogata","year":"2005","unstructured":"Ogata, K., Futatsugi, K.: Equational approach to formal analysis of TLS. In: 25th ICDCS, pp. 795\u2013804. IEEE CS Press, Los Alamitos (2005)"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: Spesification and programming language in rewriting logic. TCS\u00a0285, 187\u2013243 (2002)","journal-title":"TCS"},{"key":"7_CR12","unstructured":"Ogata, K., Kong, W., Futatsugi, K.: Falsification of OTSs by searches of bounded reachable state spaces. In: 18th SEKE, pp. 440\u2013445 (2006)"},{"key":"7_CR13","volume-title":"Advances in Computers","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers, vol.\u00a058. Academic Press, London (2003)"},{"key":"7_CR14","doi-asserted-by":"crossref","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":"7_CR15","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: Model-checking observational transition system with Maude. In: 20th ITC-CSCC, pp. 5\u20136 (2005)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BFb0036919","volume-title":"Automata, Languages and Programming","author":"J. Hsiang","year":"1983","unstructured":"Hsiang, J., Dershowitz, N.: Rewrite methods for clausal and nonclausal theorem proving. In: D\u00edaz, J. (ed.) ICALP 1983. LNCS, vol.\u00a0154, pp. 331\u2013346. Springer, Heidelberg (1983)"},{"key":"7_CR17","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":"7_CR18","volume-title":"Model Checking","author":"M. Edmund","year":"2001","unstructured":"Edmund, M., Clarke, J., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2001)"},{"key":"7_CR19","series-title":"ENTCS 71","first-page":"143","volume-title":"WRLA 2002","author":"S. Eker","year":"2002","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: WRLA 2002. ENTCS 71, pp. 143\u2013168. Elsevier, Amsterdam (2002)"},{"key":"7_CR20","unstructured":"Wang, B.Y.: Specification of an infinite-state local model checker in rewriting logic. In: 17th SEKE, pp. 442\u2013447 (2005)"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM TOPLAS\u00a016, 1512\u20131542 (1994)","journal-title":"ACM TOPLAS"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","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: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 14\u201326. Springer, Heidelberg (2003)"},{"key":"7_CR23","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":"7_CR24","first-page":"59","volume-title":"12th APSEC","author":"W. Kong","year":"2005","unstructured":"Kong, W., Ogata, K., Seino, T., Futatsugi, K.: Lightweight integration of theorem proving and model checking for system verification. In: 12th APSEC, pp. 59\u201366. IEEE CS Press, Los Alamitos (2005)"},{"key":"7_CR25","unstructured":"Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Automatic verification of the STS authentication protocol with Cr\u00e8me. In: 20th ITC-CSCC, pp. 15\u201316 (2005)"},{"key":"7_CR26","volume-title":"6th QSIC","author":"M. Nakano","year":"2006","unstructured":"Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Automating invariant verification of behavioral specifications. In: 6th QSIC. IEEE CS Press, Los Alamitos (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:00:44Z","timestamp":1558288844000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11901433_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}