{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T00:29:35Z","timestamp":1745281775090},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642546235"},{"type":"electronic","value":"9783642546242"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-642-54624-2_31","type":"book-chapter","created":{"date-parts":[[2014,2,28]],"date-time":"2014-02-28T17:42:59Z","timestamp":1393609379000},"page":"630-656","source":"Crossref","is-referenced-by-count":4,"title":["Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs"],"prefix":"10.1007","author":[{"given":"Kazuhiro","family":"Ogata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Ogata, K., Kurihara, S., Inari, M., Doi, N.: The design and implementation of HoME. In: PLDI 1992, pp. 44\u201354 (1992)","DOI":"10.1145\/143103.143117"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Ogata, K., Doi, N.: Object allocation and dynamic compilation in MultithreadSmalltalk. In: 9th SAC, pp. 452\u2013456 (1994)","DOI":"10.1145\/326619.326808"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-62950-5_84","volume-title":"Rewriting Techniques and Applications","author":"K. Ogata","year":"1997","unstructured":"Ogata, K., Ohhara, K., Futatsugi, K.: TRAM: An abstract machine for order-sorted conditional term rewriting systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 335\u2013338. Springer, Heidelberg (1997)"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1209","DOI":"10.1007\/BFb0002874","volume-title":"Euro-Par \u201997 Parallel Processing","author":"K. Ogata","year":"1997","unstructured":"Ogata, K., Kondo, M., Ioroi, S., Futatsugi, K.: Design and implementation of Parallel TRAM. In: Lengauer, C., Griebl, M., Gorlatch, S. (eds.) Euro-Par 1997. LNCS, vol.\u00a01300, pp. 1209\u20131216. Springer, Heidelberg (1997)"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/BFb0057939","volume-title":"Euro-Par\u201998 Parallel Processing","author":"K. Ogata","year":"1998","unstructured":"Ogata, K., Hirata, H., Ioroi, S., Futatsugi, K.: Experimental implementation of Parallel TRAM on massively parallel computer. In: Pritchard, D., Reeve, J. (eds.) Euro-Par 1998. LNCS, vol.\u00a01470, pp. 846\u2013851. Springer, Heidelberg (1998)"},{"key":"31_CR6","unstructured":"Ogata, K., Futatsugi, K.: Specification and verification of some classical mutual exclusion algorithms with CafeOBJ. In: OBJ\/CafeOBJ\/Maude Workshop at FM 1999, pp. 159\u2013177 (1999)"},{"key":"31_CR7","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":"31_CR8","doi-asserted-by":"crossref","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.) Goguen Festschrift. LNCS, vol.\u00a04060, pp. 596\u2013615. Springer, Heidelberg (2006)","DOI":"10.1007\/11780274_31"},{"key":"31_CR9","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. TCS\u00a0245, 55\u2013101 (2000)","journal-title":"TCS"},{"key":"31_CR10","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, 74\u201395 (2000)","journal-title":"J. UCS"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing 6. World Scientific (1998)","DOI":"10.1142\/3831"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-46674-6_24","volume-title":"Advances in Computing Science - ASIAN\u201999","author":"K. Ogata","year":"1999","unstructured":"Ogata, K., Futatsugi, K.: Formal verification of the MCS list-based queuing lock. In: Thiagarajan, P.S., Yap, R. (eds.) ASIAN 1999. LNCS, vol.\u00a01742, pp. 281\u2013293. Springer, Heidelberg (1999)"},{"key":"31_CR14","series-title":"IFIP","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-0-387-35496-5_13","volume-title":"Formal Methods for Open Object-Based Distributed Systems V","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm. In: Jacobs, B., Rensink, A. (eds.) Formal Methods for Open Object-Based Distributed Systems V. IFIP, vol.\u00a081, pp. 181\u2013195. Springer, Heildelberg (2002)"},{"key":"31_CR15","unstructured":"Xiang, J., Ogata, K., Futatsugi, K.: Formal fault tree analysis of state transition systems. In: 5th QSIC, pp. 124\u2013131 (2005)"},{"key":"31_CR16","first-page":"3","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. IJSEKE\u00a017, 3\u201332 (2007)","journal-title":"IJSEKE"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-88194-0_13","volume-title":"Formal Methods and Software Engineering","author":"K. Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of the bakery protocol with consideration of nonatomic reads and writes. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 187\u2013206. Springer, Heidelberg (2008)"},{"key":"31_CR18","doi-asserted-by":"publisher","first-page":"974","DOI":"10.1587\/transinf.E93.D.974","volume":"E93-D","author":"W. Kong","year":"2010","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: Towards reliable e-government systems with the OTS\/CafeOBJ method. IEICE Transactions\u00a0E93-D, 974\u2013984 (2010)","journal-title":"IEICE Transactions"},{"key":"31_CR19","first-page":"253","volume":"20","author":"K. Ogata","year":"2010","unstructured":"Ogata, K., Futatsugi, K.: Proof score approach to analysis of electronic commerce protocols. IJSEKE\u00a020, 253\u2013287 (2010)","journal-title":"IJSEKE"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"Zhang, M., Ogata, K., Futatsugi, K.: Formalization and verification of behavioral correctness of dynamic software updates. In: 2nd VSSE. ENTCS, vol.\u00a0294, pp. 12\u201323 (2013)","DOI":"10.1016\/j.entcs.2013.02.013"},{"key":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-540-69149-5_30","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K. Futatsugi","year":"2008","unstructured":"Futatsugi, K., Goguen, J., Ogata, K.: Verifying design with proof scores. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 277\u2013290. Springer, Heidelberg (2008)"},{"key":"31_CR22","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.tcs.2012.07.041","volume":"464","author":"K. Futatsugi","year":"2012","unstructured":"Futatsugi, K., G\u0103in\u0103, D., Ogata, K.: Principles of proof scores in CafeOBJ. TCS\u00a0464, 90\u2013112 (2012)","journal-title":"TCS"},{"key":"31_CR23","doi-asserted-by":"publisher","first-page":"2804","DOI":"10.1093\/ietisy\/e91-d.12.2804","volume":"E91-D","author":"K. Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Proof score approach to verification of liveness properties. IEICE Transactions\u00a0E91-D, 2804\u20132817 (2008)","journal-title":"IEICE Transactions"},{"key":"31_CR24","first-page":"162","volume":"66","author":"K. Ogata","year":"2007","unstructured":"Ogata, K., Futatsugi, K.: Modeling and verification of real-time systems based on equations. SCP\u00a066, 162\u2013180 (2007)","journal-title":"SCP"},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-34032-1_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"I. Ouranos","year":"2012","unstructured":"Ouranos, I., Ogata, K., Stefaneas, P.: Formal analysis of TESLA protocol in the Timed OTS\/CafeOBJ method. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol.\u00a07610, pp. 126\u2013142. Springer, Heidelberg (2012)"},{"key":"31_CR26","first-page":"783","volume":"17","author":"M. Nakano","year":"2007","unstructured":"Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Creme: An automatic invariant prover of behavioral specifications. IJSEKE\u00a017, 783\u2013804 (2007)","journal-title":"IJSEKE"},{"key":"31_CR27","first-page":"90","volume":"18","author":"D. G\u0103in\u0103","year":"2012","unstructured":"G\u0103in\u0103, D., Futatsugi, K., Ogata, K.: Constructor-based logics. J. UCS\u00a018, 90\u2013112 (2012)","journal-title":"J. UCS"},{"key":"31_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/978-3-642-40206-7_26","volume-title":"5th CALCO","author":"D. G\u0103in\u0103","year":"2013","unstructured":"G\u0103in\u0103, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol.\u00a08089, pp. 328\u2013333. Springer, Heidelberg (2013)"},{"key":"31_CR29","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":"31_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-642-16901-4_33","volume-title":"Formal Methods and Software Engineering","author":"K. Ogata","year":"2010","unstructured":"Ogata, K., Futatsugi, K.: A combination of forward & backward reachability analysis methods. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 501\u2013517. Springer, Heidelberg (2010)"},{"key":"31_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","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. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"31_CR32","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: Model-checking observational transition system with Maudea. In: 20th ITC-CSCC, pp. 5\u20136 (2005)"},{"key":"31_CR33","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":"31_CR34","doi-asserted-by":"crossref","unstructured":"Kong, W., Ogata, K., Seino, T., Futatsugi, K.: A lightweight integration of theorem proving and model checking for system verification. In: 12th APSEC, pp. 59\u201366 (2005)","DOI":"10.1109\/APSEC.2005.9"},{"key":"31_CR35","doi-asserted-by":"publisher","first-page":"1492","DOI":"10.1093\/ietisy\/e91-d.5.1492","volume":"E91-D","author":"M. Nakamura","year":"2008","unstructured":"Nakamura, M., Kong, W., Ogata, K., Futatsugi, K.: A specification translation from behavioral specifications to rewrite specifications. IEICE Transactions\u00a0E91-D, 1492\u20131503 (2008)","journal-title":"IEICE Transactions"},{"key":"31_CR36","doi-asserted-by":"publisher","first-page":"976","DOI":"10.1587\/transinf.E94.D.976","volume":"94-D","author":"M. Zhang","year":"2011","unstructured":"Zhang, M., Ogata, K., Nakamura, M.: Translation of state machines from equational theories into rewrite theories with tool support. IEICE Transactions\u00a094-D, 976\u2013988 (2011)","journal-title":"IEICE Transactions"},{"key":"31_CR37","doi-asserted-by":"crossref","unstructured":"Zhang, M., Ogata, K.: Invariant-preserved transformation of state machines from equations into rewrite rules. In: 18th APSEC, pp. 511\u2013516 (2012)","DOI":"10.1109\/APSEC.2012.99"},{"key":"31_CR38","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":"31_CR39","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":"31_CR40","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":"31_CR41","doi-asserted-by":"crossref","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action. Kluwer (2000)","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"31_CR42","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2008.04.040","volume":"403","author":"J. Meseguer","year":"2008","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. TCS\u00a0403, 239\u2013264 (2008)","journal-title":"TCS"},{"key":"31_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-22944-2_22","volume-title":"Algebra and Coalgebra in Computer Science","author":"C. Rocha","year":"2011","unstructured":"Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol.\u00a06859, pp. 314\u2013328. Springer, Heidelberg (2011)"},{"key":"31_CR44","series-title":"LNCS","first-page":"361","volume-title":"10th ICALP","author":"J.P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Diaz, J. (ed.) 10th ICALP. LNCS, vol.\u00a0154, pp. 361\u2013373. Springer, Heidelberg (1983)"},{"key":"31_CR45","first-page":"771","volume":"19","author":"K. Ogata","year":"2013","unstructured":"Ogata, K., Futatsugi, K.: Compositionally writing proof scores of invariants in the OTS\/CafeOBJ method. J. UCS\u00a019, 771\u2013804 (2013)","journal-title":"J. UCS"},{"key":"31_CR46","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: 24th RTA, pp. 81\u201396 (2013)"},{"key":"31_CR47","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":"31_CR48","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":"31_CR49","series-title":"LNCS","first-page":"101","volume-title":"DISCO 1990","author":"R. Hennicker","year":"1990","unstructured":"Hennicker, R.: Context induction: A proof principle for behavioural abstractions. In: Miola, A. (ed.) DISCO 1990. LNCS, vol.\u00a0429, pp. 101\u2013110. Springer, Heidelberg (1990)"},{"key":"31_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-03741-2_10","volume-title":"Algebra and Coalgebra in Computer Science","author":"G. Ro\u015fu","year":"2009","unstructured":"Ro\u015fu, G., Lucanu, D.: Circular coinduction: A proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 127\u2013144. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Specification, Algebra, and Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54624-2_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T06:25:28Z","timestamp":1558851928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54624-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642546235","9783642546242"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54624-2_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}