Some Papers on Maude and Rewriting Logic

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

The links below give access to abstracts of our papers and, for most of them, to dvi and/or postscript copies of the papers themselves. In some cases there are links to other sites where the papers are available.

The most recent ones come first.

Recent

Joe Hendrix and José Meseguer
Order-sorted Equational Unification Revisited.
9th International Workshop on Rule-Based Programming, July, 2008.
(PDF)

José Meseguer
Twenty Years of Rewriting Logic.
In Proc. Rewriting Techniques and Applications, 2010 , Springer-Verlag LNCS 2706, 15-17, 2010.
(PDF)

Francisco Durán and José Meseguer
On the Church-Rosser and Coherence Properties of Conditional Order-Sorted Rewrite Theories.
Journal of Logic and Algebraic Programming, Elsevier, 2012.
(PDF)

A. Riesco, A. Verdejo, R. Caballero, and N. Martí-Oliet
Declarative debugging of Maude modules.
Technical report SIC-6/08, Dpto. Sistemas Informaticos y Computacion, Universidad Complutense de Madrid, April 2008.
(Abstract) (BibTeX entry) (PDF)

A. Riesco and A. Verdejo
The EIGRP Protocol in Maude.
Technical report SIC-3/07, Dpto. Sistemas Informaticos y Computacion, Universidad Complutense de Madrid, April 2007.
(Abstract) (BibTeX entry) (PDF)

A. Riesco and A. Verdejo
Parameterized skeletons in Maude.
Technical report SIC-1/07, Dpto. Sistemas Informaticos y Computacion, Universidad Complutense de Madrid, January 2007.
(Abstract) (BibTeX entry) (PDF)

José Meseguer, Miguel Palomino and Narciso Martí-Oliet
Algebraic Simulations.
Submitted for publication.
(BibTeX entry) (PDF)

José Meseguer, Miguel Palomino and Narciso Martí-Oliet
Equational abstractions.
Submitted for publication.
(BibTeX entry) (PDF)

José Meseguer and Christiano O. Braga
Modular Rewriting Semantics of Programming Languages.
Submitted for publication.
(abstract) (BibTeX entry) (gzip'ed Postscript)

2003

Steven Eker
Associative-Commutative Rewriting on Large Terms.
In Proc. Rewriting Techniques and Applications, 2003 , Springer-Verlag LNCS 2706, 14-29, June 2003.
(abstract) (BibTeX entry) (gzip'ed Postscript) (PDF slides)

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer and Carolyn Talcott
The Maude 2.0 System.
In Proc. Rewriting Techniques and Applications, 2003 , Springer-Verlag LNCS 2706, 76-87, June 2003.
(abstract) (BibTeX entry) (gzip'ed Postscript) (PDF slides)

José Meseguer
Software Specification and Verification in Rewriting Logic.
Lectures at the Marktoberdorf International Summer School, Germany, 2002.
(abstract) (BibTeX entry) (gzip'ed Postscript)

José Meseguer, Miguel Palomino, and Narciso Martí-Oliet
Equational Abstractions.
In Proc. Nineteenth International Conference on Automated Deduction, Springer-Verlag LNCS, 2003
(abstract) (BibTeX entry) (gzip'ed Postscript)

Roberto Bruni and José Meseguer
Generalized Rewrite Theories.
In Proc. Thirtieth International Colloquium on Automata, Languages and Programming, Springer-Verlag LNCS, 2003.
(abstract) (BibTeX entry) (gzip'ed Postscript)

José Meseguer, Miguel Palomino and Narciso Martí-Oliet
Notes on Model Checking and Abstraction in Rewriting Logic.
(PDF)

2001

Alberto Verdejo and Narciso Martí-Oliet
Executing and Verifying CCS in Maude.
Submitted for publication, October 2002.
(abstract) (BibTeX entry) (gzip'ed Postscript)

José Meseguer
Rewriting Logic Revisited
Slides of tutorial presented at WRLA 2002, Pisa, Italy, September 2002.
(gzip'ed Postscript)

Steven Eker, Merrill Knapp, Keith Laderoute, Patrick Lincoln and Carolyn Talcott
Pathway Logic: Executable Models of Biological Networks
In 4th International Workshop on Rewriting Logic and its Applications (WRLA'02).
(abstract) (BibTeX entry) (gzip'ed Postscript)

Alberto Verdejo and Narciso Martí-Oliet
Implementing CCS in Maude 2.
In 4th International Workshop on Rewriting Logic and its Applications (WRLA'02).
(abstract) (BibTeX entry) (gzip'ed Postscript)

Steven Eker, José Meseguer and Ambarish Sridharanarayanan.
The Maude LTL Model Checker.
In 4th International Workshop on Rewriting Logic and its Applications (WRLA'02).
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán and Alberto Verdejo
A Conference Reviewing System in Mobile Maude.
In 4th International Workshop on Rewriting Logic and its Applications (WRLA'02).
(abstract) (BibTeX entry) (gzip'ed Postscript)

Mark-Oliver Stehr and Carolyn Talcott
Plan in Maude: Specifying an Active Network Programming Language
In 4th International Workshop on Rewriting Logic and its Applications (WRLA'02).
(abstract) (BibTeX entry) (gzip'ed Postscript)

2001

Christiano de Oliveira Braga.
Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics.
PhD thesis, Pontifícia Universidade Católica do Rio de Janeiro. September, 2001.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Narciso Martí-Oliet and José Meseguer.
Rewriting Logic: Roadmap and Bibliography.
(abstract) (BibTeX entry) (gzip'ed Postscript)

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J.F. Quesada.
Maude: Specification and Programming in Rewriting Logic.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Miguel Palomino Tarjuelo.
Relating Meseguer's Rewriting Logic with the Constructor-Based Rewriting Logic.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Mark-Oliver Stehr, José Meseguer, and Peter C. Ölveczky.
Rewriting Logic as a Unifying Framework for Petri Nets.
In Unifying Petri Nets. Lecture Notes in Computer Science (Advances in Petri Nets). 2001
(abstract) (BibTeX entry) (gzip'ed Postscript)

2000

Alberto Verdejo and Narciso Martí-Oliet.
Implementing CCS in Maude.
In T. Bolognesi and D. Latella, editors, Formal Methods For Distributed System Development. FORTE/PSTV 2000 IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX) October 10-13, 2000, Pisa, Italy, pages 351-366. Kluwer Academic Publishers, 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

F. Durán, S. Eker, P. Lincoln, and J. Meseguer.
Mobile Maude.
In D. Kotz and F. Mattern, editors, Agent Systems, Mobile Agents, and Applications, Second International Symposium on Agent Systems and Applications and Fourth International Symposium in Mobile Agents, ASA/MA 2000, LNCS 1882. Springer-Verlag, Sept. 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán and José Meseguer.
Maude's Module Algebra.
Submitted for publication, 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Peter Csaba Ölveczky.
Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic.
Doctoral Thesis. University of Bergen, 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

P. C. Ölveczky, M. Keaton, J. Meseguer, C. Talcott, and S. Zabele.
Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude.
In 4th International Conference on Fundamental Approaches to Software Engineering (FASE'01).
Lecture Notes in Computer Science, Vol. 2029, pp. 333-348. 2001
(abstract) (BibTeX entry) (gzip'ed Postscript)

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J.F. Quesada.
Towards Maude 2.0.
In 3rd International Workshop on Rewriting Logic and its Applications (WRLA'00).
Electronic Notes in Theoretical Computer Science, Vol. 36. 2000
(abstract) (BibTeX entry) (gzip'ed Postscript)

Peter Csaba Ölveczky and José Meseguer.
Real-Time Maude: A Tool for Simulating and Analyzing Real-Time and Hybrid Systems.
In 3rd International Workshop on Rewriting Logic and its Applications (WRLA'00).
Electronic Notes in Theoretical Computer Science, Vol. 36. 2000
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán and José Meseguer.
A Church-Rosser Checker Tool for Maude Equational Specifications.
Manuscript. Universidad de Málaga and SRI International. July 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán.
Termination Checker and Knuth-Bendix Completion Tools for Maude Equational Specifications.
Manuscript. Universidad de Málaga. July 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán.
Coherence Checker and Completion Tools for Maude Specifications.
Manuscript. Universidad de Málaga. July 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Manuel Clavel, Francisco Durán, Steven Eker, and José Meseguer.
Building Equational Proving Tools by Reflection in Rewriting Logic.
In Cafe: An Industrial-Strength Algebraic Formal Method.
Elsevier, 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Peter Csaba Ölveczky and José Meseguer.
Specification of Real-Time and Hybrid Systems in Rewriting Logic.
Submitted for publication, May 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada.
A Maude Tutorial.
Manuscript, March 2000.
(abstract) (BibTeX entry) (gzip'ed Postscript)

1999

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada.
Maude: Specification and Programming in Rewriting Logic.
Maude System documentation. March, 1999.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán and José Meseguer.
The Maude Specification of Full Maude.
Manuscript, May 1999.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán and José Meseguer.
Structured Theories and Institutions.
In 8th Conference on Category Theory and Computer Science (CTCS'99).
Electronic Notes in Theoretical Computer Science, Vol. 29. 1999
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán.
A Reflective Module Algebra with Applications to the Maude Language.
PhD thesis, University of Málaga. April, 1999.
(abstract) (BibTeX entry) (gzip'ed Postscript)

M. Clavel, F. Durán, S. Eker, J. Meseguer, and M.-O. Stehr.
Maude as a Formal Meta-Tool.
In World Congress on Formal Methods (FM'99).
Lecture Notes in Computer Science, Vol. 1709, pp. 1684-1703. 1999
(abstract) (BibTeX entry) (gzip'ed Postscript)

1998

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, and J. Meseguer.
Metalevel Computation in Maude.
In 2nd International Workshop on Rewriting Logic and its Applications (WRLA'98).
Electronic Notes in Theoretical Computer Science, Vol. 15. 1998
(abstract) (BibTeX entry) (gzip'ed Postscript)

Francisco Durán and José Meseguer.
An Extensible Module Algebra for Maude.
In 2nd International Workshop on Rewriting Logic and its Applications (WRLA'98).
Electronic Notes in Theoretical Computer Science, Vol. 15. 1998
(abstract) (BibTeX entry) (gzip'ed Postscript)

Steven Eker.
Term Rewriting with Operator Evaluation Strategy.
In 2nd International Workshop on Rewriting Logic and its Applications (WRLA'98).
Electronic Notes in Theoretical Computer Science, Vol. 15. 1998
(abstract) (BibTeX entry) (gzip'ed Postscript)

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada.
Maude as a Metalanguage.
In 2nd International Workshop on Rewriting Logic and its Applications (WRLA'98).
Electronic Notes in Theoretical Computer Science, Vol. 15. 1998
(abstract) (BibTeX entry) (gzip'ed Postscript)

Adel Bouhoula, Jean-Pierre Jouannaud, and José Meseguer.
Specification and Proof in Membership Equational Logic.
Manuscript, December 1998.
(abstract) (BibTeX entry) (gzip'ed Postscript)

José Meseguer.
Membership Algebra as a Logical Framework for Equational Specification.
In 12th International Workshop on Recent Trends in Algebraic Development Techniques (WADT'97),
Lecture Notes in Computer Science, Vol. 1376, pp. 18-61. 1998
(abstract) (BibTeX entry) (gzip'ed Postscript)

Grit Denker, José Meseguer, and Carolyn Talcott.
Protocol Specification and Analysis in Maude.
In Proc. of Workshop on Formal Methods and Security Protocols. 1998.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Manuel Clavel, Francisco Durán, Steven Eker, and José Meseguer.
Building Equational Proving Tools by Reflection in Rewriting Logic.
In Proceedings of the CafeOBJ Symposium '98. April, 1998.
(abstract) (BibTeX entry) (gzip'ed Postscript)

Manuel Clavel, Francisco Durán, Steven Eker, and José Meseguer.
Design and Implementation of the Cafe Prover and Church-Rosser Checker Tools.
Manuscript, March 1998
(abstract) (BibTeX entry) (gzip'ed Postscript)

José Meseguer.
Research Directions in Rewriting Logic.
Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, 1997. Springer-Verlag, 1998.
(abstract) (BibTeX entry) (gzip'ed Postscript)

1996

Manuel Clavel, Steven Eker, Patrick Lincoln, and José Meseguer.
Principles of Maude.
In 1st International Workshop on Rewriting Logic and its Applications (WRLA'96).
Electronic Notes in Theoretical Computer Science, Vol. 4. 1996
(abstract) (BibTeX entry) (gzip'ed Postscript)

Steven Eker.
Fast Matching in Combinations of Regular Equational Theories.
In 1st International Workshop on Rewriting Logic and its Applications (WRLA'96).
Electronic Notes in Theoretical Computer Science, Vol. 4. 1996
(abstract) (BibTeX entry) (gzip'ed Postscript)

Manuel Clavel and José Meseguer.
Reflection and Strategies in Rewriting Logic.
In 1st International Workshop on Rewriting Logic and its Applications (WRLA'96).
Electronic Notes in Theoretical Computer Science, Vol. 4. 1996
(abstract) (BibTeX entry) (gzip'ed Postscript)

Narciso Martí-Oliet and José Meseguer.
Rewriting Logic as a Logical and Semantic Framework.
In 1st International Workshop on Rewriting Logic and its Applications (WRLA'96).
Electronic Notes in Theoretical Computer Science, Vol. 4. 1996
(abstract) (BibTeX entry) (gzip'ed Postscript)

Peter Csaba Ölveczky and José Meseguer.
Specifying Real-Time Systems in Rewriting Logic.
In 1st International Workshop on Rewriting Logic and its Applications (WRLA'96).
Electronic Notes in Theoretical Computer Science, Vol. 4. 1996
(abstract) (BibTeX entry) (gzip'ed Postscript)

1993

Narciso Martí-Oliet and José Meseguer.
Rewriting Logic as a Logical and Semantic Framework.
Technical Report SRI-CSL-93-05, SRI International, Computer Science Laboratory, August 1993. (to appear in Handbook of Philosophical Logic), Kluwer Academic Publishers.
(abstract) (BibTeX entry) (gzip'ed Postscript)

[Maude Home Page]