{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:28Z","timestamp":1762458868238},"publisher-location":"Berlin, Heidelberg","reference-count":65,"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_1","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T17:40:06Z","timestamp":1289238006000},"page":"1-20","source":"Crossref","is-referenced-by-count":9,"title":["Fostering Proof Scores in CafeOBJ\u00a0"],"prefix":"10.1007","author":[{"given":"Kokichi","family":"Futatsugi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(96)00039-4","volume":"165","author":"M. Bidoit","year":"1996","unstructured":"Bidoit, M., Hennicker, R.: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science\u00a0165(1), 3\u201355 (1996)","journal-title":"Theoretical Computer Science"},{"key":"1_CR3","unstructured":"Burstall, R.M., Goguen, J.A.: Putting theories together to make specifications. In: IJCAI, pp. 1045\u20131058 (1977)"},{"key":"1_CR4","unstructured":"CafeOBJ: Web page (2010), http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"1_CR5","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"key":"1_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"1_CR7","series-title":"AMAST Series in Computing","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume-title":"CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol.\u00a06. World Scientific, Singapore (1998)"},{"issue":"1","key":"1_CR8","first-page":"74","volume":"6","author":"R. Diaconescu","year":"2000","unstructured":"Diaconescu, R., Futatsugi, K.: Behavioural coherence in object-oriented algebraic specification. Journal of Universal Computer Science\u00a06(1), 74\u201396 (2000)","journal-title":"Journal of Universal Computer Science"},{"issue":"2","key":"1_CR9","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/S0304-3975(01)00361-9","volume":"285","author":"R. Diaconescu","year":"2002","unstructured":"Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theor. Comput. Sci.\u00a0285(2), 289\u2013318 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K., Iida, S.: Component-based algebraic specification and verification in CafeOBJ. In: Wing et al. [65], pp. 1644\u20131663","DOI":"10.1007\/3-540-48118-4_37"},{"key":"1_CR11","unstructured":"FSSV 2010: Web page (March 2010), http:\/\/www.ldl.jaist.ac.jp\/jaist-fssv2010\/lectureMaterials\/"},{"key":"1_CR12","first-page":"139","volume-title":"Programming of Future Generation Computers","author":"K. Futatsugi","year":"1986","unstructured":"Futatsugi, K.: An overview of OBJ2. In: Fuchi, K., Nivat, M. (eds.) Programming of Future Generation Computers, pp. 139\u2013160. North-Holland, Amsterdam (1986); Proc. of Franco-Japanese Symp. on Programming of Future Generation Computers, Tokyo (October 1986)"},{"key":"1_CR13","unstructured":"Futatsugi, K.: Trends in formal specification methods based on algebraic specification techniques \u2013 from abstract data types to software processes: A personal perspective. In: Proceedings of the International Conference of Information Technology to Commemorating the 30th Anniversary of the Information Processing Society of Japan (InfoJapan 1990), pp. 59\u201366. Information Processing Society of Japan (1990) (invited talk)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45788-7_1","volume-title":"Functional and Logic Programming","author":"K. Futatsugi","year":"2002","unstructured":"Futatsugi, K.: Formal methods in CafeOBJ. In: Hu, Z., Rodr\u00edguez-Artalejo, M. (eds.) FLOPS 2002. LNCS, vol.\u00a02441, pp. 1\u201320. Springer, Heidelberg (2002)"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/ASE.2006.73","volume-title":"Proc. of 21st IEEE\/ACM International Conference on Automated Software Engineering (ASE 2006)","author":"K. Futatsugi","year":"2006","unstructured":"Futatsugi, K.: Verifying specifications with proof scores in CafeOBJ. In: Proc. of 21st IEEE\/ACM International Conference on Automated Software Engineering (ASE 2006), pp. 3\u201310. IEEE Computer Society, Los Alamitos (2006)"},{"volume-title":"OBJ\/CafeOBJ\/Maude at Formal Methods 1999","year":"1999","key":"1_CR16","unstructured":"Futatsugi, K., Goguen, J., Meseguer, J. (eds.): OBJ\/CafeOBJ\/Maude at Formal Methods 1999. The Theta Foundation, Bucharest (1999) ISBN 973-99097-1-X"},{"key":"1_CR17","first-page":"52","volume-title":"Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages (POPL 1985)","author":"K. Futatsugi","year":"1985","unstructured":"Futatsugi, K., Goguen, J.A., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages (POPL 1985), New Orleans, Louisiana, pp. 52\u201366. ACM, New York (1985)"},{"key":"1_CR18","unstructured":"Futatsugi, K., Goguen, J.A., Meseguer, J., Okada, K.: Parameterized programming in OBJ2. In: ICSE, pp. 51\u201360 (1987)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K. Futatsugi","year":"2008","unstructured":"Futatsugi, K., Goguen, J.A., Ogata, K.: Verifying design with proof scores. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, Springer, Heidelberg (2008)"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday","year":"2006","unstructured":"Futatsugi, K., Jouannaud, J.P., Meseguer, J. (eds.): Algebra, Meaning, and Computation. LNCS, vol.\u00a04060. Springer, Heidelberg (2006)"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/ICFEM.1997.630424","volume-title":"Proc. of 1st International Conference on Formal Engineering Methods (ICFEM 1997)","author":"K. Futatsugi","year":"1997","unstructured":"Futatsugi, K., Nakagawa, A.: An overview of CAFE specification environment - an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In: Proc. of 1st International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, November 12-14, pp. 170\u2013182. IEEE, Los Alamitos (1997)"},{"volume-title":"CAFE: An Industrial-Strength Algebraic Formal Method","year":"2000","key":"1_CR22","unstructured":"Futatsugi, K., Nakagawa, A., Tamai, T. (eds.): CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier Science B.V., Amsterdam (2000) ISBN 0-444-50556-3"},{"key":"1_CR23","unstructured":"Futatsugi, K., Ogata, K.: Rewriting can verify distributed real-time systems. In: Proc. of International Symposium on Rewriting, Proof, and Computation (PRC 2001), pp. 60\u201379. Tohoku Univ. (2001)"},{"key":"1_CR24","unstructured":"Futatsugi, K., Okada, K.: Specification writing as construction of hierarchically structured clusters of operators. In: IFIP Congress, pp. 287\u2013292 (1980)"},{"key":"1_CR25","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":"1_CR26","unstructured":"Goguen, J.: Hidden algebraic engineering. In: Nehaniv, C., Ito, M. (eds.) Algebraic Engineering. pp. 17\u201336. World Scientific, Singapore (1998), papers from a conference at the University of Aizu, Japan, 24\u201326 March 1997; also UCSD Technical Report CS97\u2013569 (December 1997)"},{"key":"1_CR27","unstructured":"Goguen, J.: Theorem Proving and Algebra. [Unpublished Book] (now being planned to be up on the web for the free use)"},{"issue":"1","key":"1_CR28","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S0304-3975(99)00275-3","volume":"245","author":"J. Goguen","year":"2000","unstructured":"Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science\u00a0245(1), 55\u2013101 (2000)","journal-title":"Theoretical Computer Science"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-1-4757-6541-0_1","volume-title":"Software Engineering with OBJ: Algebraic Specification in Action","author":"J. Goguen","year":"2000","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action, pp. 3\u2013167. Kluwer, Dordrecht (2000)"},{"issue":"1","key":"1_CR30","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM\u00a039(1), 95\u2013146 (1992)","journal-title":"J. ACM"},{"issue":"3","key":"1_CR31","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1017\/S0960129500000517","volume":"4","author":"J.A. Goguen","year":"1994","unstructured":"Goguen, J.A., Diaconescu, R.: An oxford survey of order sorted algebra. Mathematical Structures in Computer Science\u00a04(3), 363\u2013392 (1994)","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR32","first-page":"55","volume-title":"Proc. of 1997 International Conference on Automated Software Engineering (ASE 1997)","author":"J.A. Goguen","year":"1997","unstructured":"Goguen, J.A., Lin, K., Mori, A., Rosu, G., Sato, A.: Distributed cooperative formal methods tools. In: Proc. of 1997 International Conference on Automated Software Engineering (ASE 1997), Lake Tahoe, CA, November 02-05, pp. 55\u201362. IEEE, Los Alamitos (1997)"},{"key":"1_CR33","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1188.001.0001","volume-title":"Algebraic Semantics of Imperative Programs","author":"J.A. Goguen","year":"1996","unstructured":"Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)"},{"key":"1_CR34","first-page":"295","volume-title":"Logic Programming: Functions, Relations, and Equations","author":"J.A. Goguen","year":"1986","unstructured":"Goguen, J.A., Meseguer, J.: Eqlog: Equality, types, and generic modules for logic programming. In: DeGroot, D., Lindstrom, G. (eds.) Logic Programming: Functions, Relations, and Equations, pp. 295\u2013363. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"1_CR35","first-page":"417","volume-title":"Research Directions in Object-Oriented Programming","author":"J.A. Goguen","year":"1987","unstructured":"Goguen, J.A., Meseguer, J.: Unifying functional, object-oriented and relational programming with logical semantics. In: Shriver, B., Wegner, P. (eds.) Research Directions in Object-Oriented Programming, pp. 417\u2013478. MIT Press, Cambridge (1987)"},{"issue":"2","key":"1_CR36","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci.\u00a0105(2), 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"J.V. Guttag","year":"1993","unstructured":"Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, Heidelberg (1993)"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-49253-4_20","volume-title":"Algebraic Methodology and Software Technology","author":"R. Hennicker","year":"1998","unstructured":"Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 263\u2013277. Springer, Heidelberg (1998)"},{"key":"1_CR39","first-page":"222","volume":"62","author":"B. Jacobs","year":"1997","unstructured":"Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bulletin of the European Association for Theoretical Computer Science\u00a062, 222\u2013259 (1997)","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-540-73210-5_21","volume-title":"Integrated Formal Methods","author":"W. Kong","year":"2007","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: Algebraic approaches to formal analysis of the mondex electronic purse system. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 393\u2013412. Springer, Heidelberg (2007)"},{"issue":"1","key":"1_CR41","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1142\/S0218194007003124","volume":"17","author":"W. Kong","year":"2007","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: Specification and verification of workflows with Rbac mechanism and Sod constraints. International Journal of Software Engineering and Knowledge Engineering\u00a017(1), 3\u201332 (2007)","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"1_CR42","unstructured":"Maude: Web page (2010), http:\/\/maude.cs.uiuc.edu\/"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects. In: OOPSLA\/ECOOP, pp. 101\u2013115 (1990)","DOI":"10.1145\/97945.97958"},{"issue":"1","key":"1_CR44","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci.\u00a096(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: From OBJ to Maude and beyond. In: Futatsugi et al. [20], pp. 252\u2013280","DOI":"10.1007\/11780274_14"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Mori, A., Futatsugi, K.: Verifying behavioural specifications in CafeOBJ environment. In: Wing et al. [65], pp. 1625\u20131643","DOI":"10.1007\/3-540-48118-4_36"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/3-540-36532-X_26","volume-title":"Software Security \u2013 Theories and Systems","author":"A. Mori","year":"2003","unstructured":"Mori, A., Futatsugi, K.: CafeOBJ as a tool for behavioral system verification. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 461\u2013470. Springer, Heidelberg (2003)"},{"issue":"6","key":"1_CR49","doi-asserted-by":"publisher","first-page":"783","DOI":"10.1142\/S0218194007003458","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. International Journal of Software Engineering and Knowledge Engineering\u00a017(6), 783\u2013804 (2007)","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"1_CR51","unstructured":"Ogata, K., Futatsugi, K.: Specification and verification of some classical mutual exclusion algorithms with CafeOBJ. In: Futatsugi et al. [16], pp. 159\u2013177 ISBN 973-99097-1-X"},{"key":"1_CR52","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1109\/ASE.2001.989804","volume-title":"Proceedings of the 16th International Conference on Automated Software Engineering (16th ASE)","author":"K. Ogata","year":"2001","unstructured":"Ogata, K., Futatsugi, K.: Modeling and verification of distributed real-time systems based on CafeOBJ. In: Proceedings of the 16th International Conference on Automated Software Engineering (16th ASE), pp. 185\u2013192. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"1_CR53","first-page":"150","volume-title":"Proceedings of the 6th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (6th FMPPTA); Part of Proceedings of the 15th IPDPS","author":"K. Ogata","year":"2001","unstructured":"Ogata, K., Futatsugi, K.: Specifying and verifying a railroad crossing with CafeOBJ. In: Proceedings of the 6th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (6th FMPPTA); Part of Proceedings of the 15th IPDPS, p. 150. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"1_CR54","series-title":"ENTCS","first-page":"189","volume-title":"4th WRLA","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: 4th WRLA. ENTCS, vol.\u00a071, pp. 189\u2013203. Elsevier, Amsterdam (2002)"},{"issue":"2","key":"1_CR55","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0020-0190(02)00480-5","volume":"86","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Flaw and modification of the iKP electronic payment protocols. Information Processing Letters\u00a086(2), 57\u201362 (2003)","journal-title":"Information Processing Letters"},{"key":"1_CR56","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":"1_CR57","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":"1_CR58","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":"1_CR59","first-page":"50","volume-title":"Proceedings of the 4th International Conference on Quality Software (4th QSIC)","author":"K. Ogata","year":"2004","unstructured":"Ogata, K., Futatsugi, K.: Equational approach to formal verification of SET. In: Proceedings of the 4th International Conference on Quality Software (4th QSIC), pp. 50\u201359. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"1_CR60","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":"1_CR61","doi-asserted-by":"crossref","unstructured":"Ogata, K., Futatsugi, K.: Some tips on writing proof scores in the OTS\/CafeOBJ method. In: Futatsugi et al. [20], pp. 596\u2013615","DOI":"10.1007\/11780274_31"},{"key":"1_CR62","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2008.02.018","volume":"201","author":"K. Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the ots\/cafeobj ethod. Electr. Notes Theor. Comput. Sci.\u00a0201, 127\u2013154 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"1_CR63","volume-title":"Proc. of 12th International Conference on Formal Engineering Methods (ICFEM 2010)","author":"K. Ogata","year":"2010","unstructured":"Ogata, K., Futatsugi, K.: A combination of forward & backward reachability analysis method. In: Proc. of 12th International Conference on Formal Engineering Methods (ICFEM 2010), Shanghai, China, November 16-19. Springer, Heidelberg (2010) (to appear)"},{"key":"1_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-540-45236-2_2","volume-title":"FME 2003: Formal Methods","author":"T. Sawada","year":"2003","unstructured":"Sawada, T., Kishida, K., Futatsugi, K.: Past, present, and future of SRA implementation of CafeOBJ: Annex. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 7\u201317. Springer, Heidelberg (2003)"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","volume-title":"FM\u201999 - Formal Methods","year":"1999","unstructured":"Wing, J.M., Woodcock, J., Davies, J. (eds.): FM 1999. LNCS, vol.\u00a01709. Springer, Heidelberg (1999)"}],"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_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,13]],"date-time":"2020-06-13T16:36:51Z","timestamp":1592066211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}