{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:36Z","timestamp":1725516516712},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_30","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"277-290","source":"Crossref","is-referenced-by-count":12,"title":["Verifying Design with Proof Scores"],"prefix":"10.1007","author":[{"given":"Kokichi","family":"Futatsugi","sequence":"first","affiliation":[]},{"given":"Joseph A.","family":"Goguen","sequence":"additional","affiliation":[]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","volume-title":"Security Engineering: A Guide to Building Dependable Distributed Systems","author":"R. Anderson","year":"2001","unstructured":"Anderson, R.: Security Engineering: A Guide to Building Dependable Distributed Systems. John Wiley & Sons, Inc. NY (2001)"},{"issue":"1","key":"30_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":"30_CR3","unstructured":"CafeOBJ. CafeOBJ web page (2005), http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"30_CR4","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":"30_CR5","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":"30_CR6","volume-title":"AMAST Series in Computing, 6","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. In: AMAST Series in Computing, 6, World Scientific, Singapore (1998)"},{"issue":"1","key":"30_CR7","first-page":"74","volume":"6","author":"R. Diaconescu","year":"2000","unstructured":"Diaconescu, R., Futatsugi, K.: Behavioural coherence in object-oriented algebraic specification. J. UCS\u00a06(1), 74\u201396 (2000)","journal-title":"J. UCS"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1644","DOI":"10.1007\/3-540-48118-4_37","volume-title":"FM\u201999 - Formal Methods","author":"R. Diaconescu","year":"1999","unstructured":"Diaconescu, R., Futatsugi, K., Iida, S.: Component-based algebraic specification and verification in CafeOBJ. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1644\u20131663. Springer, Heidelberg (1999)"},{"key":"30_CR9","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":"30_CR10","first-page":"52","volume-title":"Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, (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, New Orleans, Louisiana (POPL 1985), pp. 52\u201366. ACM, New York (1985)"},{"key":"30_CR11","unstructured":"Futatsugi, K., Ogata, K.: Rewriting can verify distributed real-time systems. In: Proc. of International Symposium on Rewriting, Proof, and Computation (PRC2001), Tohoku Univ, pp. 60\u201379 (2001)"},{"key":"30_CR12","unstructured":"Goguen, J.: Hidden algebraic engineering. In: Chrystopher Nehaniv and Masami Ito, editors, Algebraic Engineering, pp. 17\u201336. World Scientific, 1998. Papers from a conference at the University of Aizu, Japan, 24\u201326 March 1997; also UCSD Technical Report CS97\u2013569 (December 1997)"},{"key":"30_CR13","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/MMSE.2000.897186","volume-title":"Proceedings, International Symposium on Multimedia Software Engineering","author":"J. Goguen","year":"2000","unstructured":"Goguen, J., Lin, K.: Web-based multimedia support for distributed cooperative software engineering. In: Proceedings, International Symposium on Multimedia Software Engineering, Papers from a conference Held in Taipei, Taiwan, pp. 25\u201332. IEEE Press, Los Alamitos (2000)"},{"key":"30_CR14","first-page":"216","volume-title":"Proceedings of Conference on Quality Software","author":"J. Goguen","year":"2003","unstructured":"Goguen, J., Lin, K.: Behavioral verification of distributed concurrent systems with BOBJ. In: Ehrich, H.-D., Tse, T.H. (eds.) Proceedings of Conference on Quality Software, pp. 216\u2013235. IEEE Press, Los Alamitos (2003)"},{"issue":"1","key":"30_CR15","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":"30_CR16","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/s001650200013","volume":"13","author":"J. Goguen","year":"2002","unstructured":"Goguen, J., Ro\u015fu, G.: Institution morphisms. Formal Aspects of Computing\u00a013, 274\u2013307 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-40020-2_12","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J.A. Goguen","year":"2003","unstructured":"Goguen, J.A., Ro\u015fu, G., Lin, K.: Conditional Circular Coinductive Rewriting with Case Analysis. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol.\u00a02755, pp. 216\u2013232. Springer, Heidelberg (2003)"},{"key":"30_CR18","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. Technical Report SRI-CSL-92-03, SRI International, Computer Science Laboratory (1992)"},{"key":"30_CR19","first-page":"55","volume-title":"Proc. of 1997 International Conference on Automated Software Engineering (ASE 1997), Lake Tahoe, CA","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, 1997, pp. 55\u201362. IEEE, Los Alamitos (1997)"},{"key":"30_CR20","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":"30_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-49253-4_25","volume-title":"Algebraic Methodology and Software Technology","author":"M. Bidoit","year":"1998","unstructured":"Bidoit, M., Hennicker, R.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 263\u2013277. Springer, Heidelberg (1998)"},{"key":"30_CR22","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":"30_CR23","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1145\/781131.781156","volume-title":"PLDI","author":"S. Lerner","year":"2003","unstructured":"Lerner, S., Millstein, T.D., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: PLDI, pp. 220\u2013231. ACM, New York (2003)"},{"key":"30_CR24","unstructured":"Maude. Maude web page (2005), http:\/\/maude.cs.uiuc.edu\/"},{"key":"30_CR25","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)"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Automating invariant verification of behavioral specifications (2005) (to be published)","DOI":"10.1109\/QSIC.2006.17"},{"key":"30_CR27","unstructured":"Ogata, K., Futatsugi, K.: Specification and verification of some classical mutual exclusion algorithms with CafeOBJ. In: Proceedings of OBJ\/CafeOBJ\/Maude Workshop at Formal Methods 1999, Theta, pp. 159\u2013177 (1999)"},{"key":"30_CR28","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":"30_CR29","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":"30_CR30","volume-title":"Proceedings of the 4th International Workshop on Rewriting Logic and its Applications (4th WRLA), ENTCS 71","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: Proceedings of the 4th International Workshop on Rewriting Logic and its Applications (4th WRLA), ENTCS 71, Elsevier, Amsterdam (2002)"},{"key":"30_CR31","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":"30_CR32","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":"30_CR33","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":"30_CR34","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":"30_CR35","unstructured":"Ogata, K., Futatsugi, K.: Proof score approach to verification of liveness properties. In: 17th International Conference on Software Engineering and Knowledge Engineering (17th SEKE), pp. 608\u2013613 (2005)"},{"key":"30_CR36","volume-title":"Proceedings of the 6th International Workshop on Rule-Based Programming (RULE\u201905), Electronic Notes in Theoretical Computer Science (ENTCS)","author":"T. Seino","year":"2005","unstructured":"Seino, T., Ogata, K., Futatsugi, K.: A toolkit for generating and displaying proof scores in the OTS\/CafeOBJ method. In: Proceedings of the 6th International Workshop on Rule-Based Programming (RULE\u201905), Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, Amsterdam (2005)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T14:44:20Z","timestamp":1684507460000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}