{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T13:02:50Z","timestamp":1746709370245},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319155449"},{"type":"electronic","value":"9783319155456"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-15545-6_13","type":"book-chapter","created":{"date-parts":[[2015,3,4]],"date-time":"2015-03-04T21:19:15Z","timestamp":1425503955000},"page":"171-192","source":"Crossref","is-referenced-by-count":7,"title":["Generate & Check Method for Verifying Transition Systems in CafeOBJ\u00a0"],"prefix":"10.1007","author":[{"given":"Kokichi","family":"Futatsugi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) RTA. LIPIcs, vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"13_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking, pp. 1\u2013975. MIT Press (2008)"},{"key":"13_CR3","unstructured":"CafeOBJ (2014), \n                    \n                      http:\/\/cafeobj.org\/\n                    \n                    \n                  , \n                    \n                      http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Parallel program design - a foundation. Addison-Wesley (1989)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"13_CR6","unstructured":"Coq (2014), \n                    \n                      http:\/\/coq.inria.fr"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods and Software Engineering","year":"2010","unstructured":"Dong, J.S., Zhu, H. (eds.): ICFEM 2010. LNCS, vol.\u00a06447. Springer, Heidelberg (2010)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-73449-9_13","volume-title":"Term Rewriting and Applications","author":"S. Escobar","year":"2007","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 153\u2013168. Springer, Heidelberg (2007)"},{"key":"13_CR9","doi-asserted-by":"crossref","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 (2006)","DOI":"10.1109\/ASE.2006.73"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Futatsugi, K.: Fostering proof scores in CafeOBJ. In: Dong, Zhu (eds.) [7], pp. 1\u201320","DOI":"10.1007\/978-3-642-16901-4_1"},{"key":"13_CR11","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. Theor. Comput. Sci.\u00a0464, 90\u2013112 (2012)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"13_CR12","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":"13_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"25 Years of Model Checking","year":"2008","unstructured":"Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol.\u00a05000. Springer, Heidelberg (2008)"},{"key":"13_CR14","doi-asserted-by":"crossref","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 (1993)","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"13_CR15","unstructured":"HOL (2014), \n                    \n                      http:\/\/hol.sourceforge.net"},{"key":"13_CR16","unstructured":"Maude (2014), \n                    \n                      http:\/\/maude.cs.uiuc.edu\/"},{"issue":"7-8","key":"13_CR17","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J. Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program.\u00a081(7-8), 721\u2013781 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-54624-2_5","volume-title":"Specification, Algebra, and Software","author":"M. Nakamura","year":"2014","unstructured":"Nakamura, M., Ogata, K., Futatsugi, K.: Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol.\u00a08373, pp. 92\u2013109. Springer, Heidelberg (2014)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"13_CR20","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":"13_CR21","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 method. Electr. Notes Theor. Comput. Sci.\u00a0201, 127\u2013154 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Ogata, K., Futatsugi, K.: A combination of forward and backward reachability analysis methods. In: Dong, Zhu (eds.) [7], pp. 501\u2013517 (2010)","DOI":"10.1007\/978-3-642-16901-4_33"},{"key":"13_CR23","unstructured":"PVS (2014), \n                    \n                      http:\/\/pvs.csl.sri.com"},{"key":"13_CR24","unstructured":"Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. technical report. Tech. rep., University of Illinois at Urbana-Champaign (2010)"},{"key":"13_CR25","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":"13_CR26","unstructured":"TeReSe (ed.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press (2003)"}],"container-title":["Lecture Notes in Computer Science","Software, Services, and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15545-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T09:13:51Z","timestamp":1559121231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-15545-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319155449","9783319155456"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15545-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}