{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:57Z","timestamp":1761597237422},"publisher-location":"Berlin, Heidelberg","reference-count":13,"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_44","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T12:40:06Z","timestamp":1289220006000},"page":"678-693","source":"Crossref","is-referenced-by-count":3,"title":["Specification Translation of State Machines from Equational Theories into Rewrite Theories"],"prefix":"10.1007","author":[{"given":"Min","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]},{"given":"Masaki","family":"Nakamura","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"44_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D. Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 480\u2013500. Springer, Heidelberg (2007)"},{"key":"44_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-05089-3_16","volume-title":"FM 2009: Formal Methods","author":"R. Eshuis","year":"2009","unstructured":"Eshuis, R.: Translating safe Petri nets to statecharts in a structure-preserving way. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 239\u2013255. Springer, Heidelberg (2009)"},{"key":"44_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-00255-7_16","volume-title":"Integrated Formal Methods","author":"P. Vargas","year":"2009","unstructured":"Vargas, P., et al.: Model Checking LTL Formulae in RAISE with FDR. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 231\u2013245. Springer, Heidelberg (2009)"},{"key":"44_CR4","doi-asserted-by":"publisher","DOI":"10.1142\/3831","volume-title":"CafeOBJ Report","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ Report. World Scientific, Singapore (1998)"},{"key":"44_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"All about Maude","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., et al.: All about Maude. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"44_CR6","first-page":"257","volume":"22","author":"R. Diaconescu","year":"2003","unstructured":"Diaconescu, R., Futatsugi, K., Ogata, K.: CafeOBJ: Logical foundations and methodologies. Computing and Informatics\u00a022, 257\u2013283 (2003)","journal-title":"Computing and Informatics"},{"key":"44_CR7","volume-title":"The SPIN model checker","author":"G. Holzmann","year":"2004","unstructured":"Holzmann, G.: The SPIN model checker. Addison-Wesley, Reading (2004)"},{"key":"44_CR8","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":"44_CR9","doi-asserted-by":"crossref","unstructured":"Kong, W., Ogata, K., et al.: 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":"44_CR10","doi-asserted-by":"publisher","first-page":"1492","DOI":"10.1093\/ietisy\/e91-d.5.1492","volume":"91-D","author":"M. Nakamura","year":"2008","unstructured":"Nakamura, M., Kong, W., et al.: A Specification Translation from Behavioral Specifications to Rewrite Specifications. IEICE Transactions\u00a091-D, 1492\u20131503 (2008)","journal-title":"IEICE Transactions"},{"key":"44_CR11","doi-asserted-by":"crossref","unstructured":"Zhang, M., Ogata, K.: Modular implementation of a translator from behavioral specifications to rewrite theory specifications. In: 9th QSIC, pp. 406\u2013411 (2009)","DOI":"10.1109\/QSIC.2009.60"},{"key":"44_CR12","doi-asserted-by":"crossref","unstructured":"Sipser, M.: Introduction to the Theory of Computation. PWS Pub. Co. (1996)","DOI":"10.1145\/230514.571645"},{"key":"44_CR13","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. CACM\u00a021, 993\u2013999 (1978)","journal-title":"CACM"}],"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_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T00:12:40Z","timestamp":1559779960000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}