{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:50Z","timestamp":1762458590781},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540738572"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73859-6_12","type":"book-chapter","created":{"date-parts":[[2007,8,21]],"date-time":"2007-08-21T11:37:02Z","timestamp":1187696222000},"page":"173-178","source":"Crossref","is-referenced-by-count":25,"title":["The Maude Formal Tool Environment"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Clavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francisco","family":"Dur\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joe","family":"Hendrix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salvador","family":"Lucas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"\u00d6lveczky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"12_CR1","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Th. Comp. Sci.\u00a0285(2), 187\u2013243 (2002)","journal-title":"Th. Comp. Sci."},{"key":"12_CR2","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude, A High-Performance Logical Framework. LNCS, vol.\u00a04350 (to appear)"},{"key":"12_CR3","volume-title":"CAFE: An Industrial-Strength Alg. Formal Method","author":"M. Clavel","year":"2000","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Alg. Formal Method, Elsevier, Amsterdam (2000)"},{"issue":"11","key":"12_CR4","first-page":"1618","volume":"12","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. J. of Universal Computer Science\u00a012(11), 1618\u20131650 (2007)","journal-title":"J. of Universal Computer Science"},{"key":"12_CR5","unstructured":"Clavel, M., Palomino, M., Santa-Cruz, J.: Integrating decision procedures in reflective rewriting-based theorem provers. In: Antoy, S., Toyama, Y. (eds.) Procs. WRS 2004 (2004)"},{"key":"12_CR6","unstructured":"Contejean, E., March\u00e9, C., Monate, B., Urbain, X.: Proving termination of rewriting with CiME. In: Rubio, A. (ed.) Procs. of WST 2003, pp. 71\u201373 (2003)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J., March\u00e9, C., Urbain, X.: Proving termination of membership equational programs. In: Sestoft, P., Heintze, N. (eds.) Procs. PEPM 2004 (2004)","DOI":"10.1145\/1014007.1014022"},{"key":"12_CR8","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J., March\u00e9, C., Urbain, X.: Proving operational termination of membership equational programs. Higher-Order and Symb. Comp. (to appear)"},{"issue":"2","key":"12_CR9","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2006.07.002","volume":"66","author":"F. Dur\u00e1n","year":"2007","unstructured":"Dur\u00e1n, F., Meseguer, J.: Maude\u2019s Module Algebra. Science of Computer Programming\u00a066(2), 125\u2013153 (2007)","journal-title":"Science of Computer Programming"},{"key":"12_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"12_CR11","unstructured":"Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. Tech. Report UIUCDCS-R-2007-2812, U. of Illinois (2007)"},{"key":"12_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11814771_14","volume-title":"Automated Reasoning","author":"J. Hendrix","year":"2006","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 151\u2013155. Springer, Heidelberg (2006)"},{"key":"12_CR13","unstructured":"Hendrix, J., Ohsaki, H., Meseguer, J.: Sufficient completeness checking with propositional tree automata. Tech. Report UIUCDCS-R-2005-2635, U. of Illinois (2005)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11805618_5","volume-title":"Term Rewriting and Applications","author":"J. Hendrix","year":"2006","unstructured":"Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 50\u201365. Springer, Heidelberg (2006)"},{"issue":"2","key":"12_CR15","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Zhang, H.: An overview of rewrite rule laboratory (RRL). J.\u00a0Computer and Mathematics with Applications\u00a029(2), 91\u2013114 (1995)","journal-title":"J.\u00a0Computer and Mathematics with Applications"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-25979-4_14","volume-title":"Rewriting Techniques and Applications","author":"S. Lucas","year":"2004","unstructured":"Lucas, S.: MU-TERM: A tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 200\u2013209. Springer, Heidelberg (2004)"},{"key":"12_CR17","unstructured":"March\u00e9, C., Rubio, A., Zantema, H.: The Termination Problems Data Base: format of input files (March 2005), Available at http:\/\/www.lri.fr\/~marche\/tpdb\/"},{"key":"12_CR18","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. In: Procs. WRLA 2006 (2006)"},{"issue":"1\/2","key":"12_CR19","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symb. Comp.\u00a020(1\/2), 161\u2013196 (2007)","journal-title":"Higher-Order and Symb. Comp."},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-006-0015-0","volume":"29","author":"P.C. \u00d6lveczky","year":"2006","unstructured":"\u00d6lveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER\/NCA active network protocol suite in Real-Time Maude. Formal Methods in System Design\u00a029, 253\u2013293 (2006)","journal-title":"Formal Methods in System Design"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude. In: FMOOD 2007 (to appear)","DOI":"10.1109\/IPDPS.2006.1639414"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BFb0012831","volume-title":"9th International Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Lusk, E., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. LNCS, vol.\u00a0310, pp. 162\u2013181. Springer, Heidelberg (1988)"}],"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-540-73859-6_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:03:22Z","timestamp":1619517802000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73859-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540738572"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73859-6_12","relation":{},"subject":[]}}