{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T22:58:30Z","timestamp":1790722710151,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642229435","type":"print"},{"value":"9783642229442","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22944-2_22","type":"book-chapter","created":{"date-parts":[[2011,8,25]],"date-time":"2011-08-25T01:45:59Z","timestamp":1314236759000},"page":"314-328","source":"Crossref","is-referenced-by-count":21,"title":["Proving Safety Properties of Rewrite Theories"],"prefix":"10.1007","author":[{"given":"Camilo","family":"Rocha","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1-3","key":"22_CR1","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R. Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science\u00a0360(1-3), 386\u2013414 (2006)","journal-title":"Theoretical Computer Science"},{"key":"22_CR2","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":"22_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"22_CR4","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., Bevilacqua, V., Talcott, C.: All About Maude - A High-Performance Logical Framework, 1st edn. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)","edition":"1"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-16310-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F. Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A church-rosser checker tool for conditional order-sorted equational maude specifications. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 69\u201385. Springer, Heidelberg (2010)"},{"key":"22_CR6","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., Bevilacqua, V.: 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":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11784180_13","volume-title":"Algebraic Methodology and Software Technology","author":"A. Farzan","year":"2006","unstructured":"Farzan, A., Meseguer, J.: State space reduction of rewrite theories using invisible transitions. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 142\u2013157. Springer, Heidelberg (2006)"},{"key":"22_CR8","unstructured":"Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis. University of Illinois at Urbana-Champaign (April 2008)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0036921","volume-title":"Automata, Languages and Programming","author":"J.-P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: D\u00edaz, J. (ed.) ICALP 1983. LNCS, vol.\u00a0154, pp. 361\u2013373. Springer, Heidelberg (1983)"},{"key":"22_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)"},{"key":"22_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, New York (1995)"},{"issue":"1","key":"22_CR12","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.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"2-3","key":"22_CR14","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. Theoretical Computer Science\u00a0403(2-3), 239\u2013264 (2008)","journal-title":"Theoretical Computer Science"},{"key":"22_CR15","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":"22_CR16","unstructured":"Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. Technical report. University of Illinois at Urbana-Champaign (2010), \n                    \n                      http:\/\/hdl.handle.net\/2142\/17407"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-13977-2_12","volume-title":"Tests and Proofs","author":"V. Rusu","year":"2010","unstructured":"Rusu, V.: Combining theorem proving and narrowing for rewriting-logic specifications. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol.\u00a06143, pp. 135\u2013150. Springer, Heidelberg (2010)"},{"key":"22_CR18","first-page":"317","volume":"7.2","author":"V. Rusu","year":"2009","unstructured":"Rusu, V., Clavel, M.: V\u00e9rification d\u2019invariants pour des syst\u00e8mes sp\u00e9cifi\u00e9s en logique de r\u00e9\u00e9criture. Vingti\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs\u00a07.2, 317\u2013350 (2009)","journal-title":"Vingti\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-45319-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tiwari","year":"2001","unstructured":"Tiwari, A., Rue\u00df, H., Sa\u00efdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 113\u2013127. Springer, Heidelberg (2001)"},{"key":"22_CR20","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science\u00a0285, 487\u2013517 (2002)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Algebra and Coalgebra in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22944-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:13:02Z","timestamp":1558296782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22944-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642229435","9783642229442"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22944-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}