Papers: José Meseguer's group

Foundations

• Santiago Escobar, José Meseguer, and Prasanna Thati.
  Natural Rewriting for General Term Rewriting Systems.
  In S. Etalle, ed., Preproceedings of 14th Intl. Workshop on Logic-based Program Synthesis and Transformation, LOPSTR'04, 2004.

• Santiago Escobar, José Meseguer, and Prasanna Thati.
  A General Natural Rewriting Strategy.
  In Proc. IV Jornadas sobre Programacion y Lenguajes (PROLE'04), Spain, 2004.

• José Meseguer, Miguel Palomino and Narciso Martí-Oliet.
  Theoroidal Maps as Algebraic Simulations (PS).
  To appear in Proceedings of WADT'04, Springer-Verlag LNCS, 2004.

• Mark-Oliver Stehr and José Meseguer.
  Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework (PS).
  In Festschrift in Honour of Ole-Johan Dahl, Springer-Verlag LNCS, Vol. 2635, 2004.

• David Basin, Manuel Clavel and José Meseguer.
  Reflective Metalogical Frameworks (PS).
  In Proceedings of the ACM Transactions on Computer Logic, Vol. 15, pages 528-576, 2004.

• Roberto Bruni, José Meseguer, Ugo Montanari and Vladimiro Sassone.
  Algebraic Theories for Contextual Pre-nets (PS).
  In Proceedings of ICTCS 2003, 8th Italian Conference on Theoretical Computer Science, Bertinoro, Italy, Springer-Verlag LNCS, Vol. 2841, pages 256-270, October 2003.
  

• Grigore Rosu, Steven Eker, Patrick Lincoln and José Meseguer.
  Certifying and Synthesizing Membership Equational Proofs.
  In Proceedings of FM'03, Pisa, Italy, Septemer 2003.

• Roberto Bruni, José Meseguer and Ugo Montanari.
  Tiling Transactions (PS).
  In Proceedings of 4th International Workshop on Rewriting Logic and its Applications (WRLA'02) Portland, Oregon, May 2003.

• Manuel Clavel, José Meseguer and Miguel Palomino.
  Reflection in Membership Equational Logic, Horn Logic with Equality, and Rewriting Logic (PS).
  In Proceedings of 4th International Workshop on Rewriting Logic and its Applications (WRLA'02) Portland, Oregon, May 2003.

• José Meseguer, Miguel Palomino and Narciso Martí-Oliet.
  Equational Abstractions (PS).
  In Proceedings of 19th International Conference on Automated Deduction, Springer-Verlag LNCS, 2003.

• Roberto Bruni and José Meseguer.
  Generalized Rewrite Theories (PS).
  In Proceedings of 30th International Colloquium on Automata, Languages and Programming, Springer-Verlag, LNCS, 2003.

• José Meseguer and Francisco Durán.
  Structured Theories and Institutions.
  Theoretical Computer Science, Vol. 309, pages 357-380, 2003.

• José Meseguer and Grigore Rosu.
  A Total Approach to Partial Algebraic Specification.
  In Proceedings of the International Conference on Automata, Languages, and Programming (ICALP'02), Málaga, Spain, July 2002. Springer-Verlag LNCS, Vol. 2380, pages 572-584, 2002.

Maude System and Applications

• Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer and Carolyn Talcott.
  The Maude 2.0 System.
  In Proceedings of Rewriting Techniques and Applications, 2003, Springer-Verlag LNCS, Vol. 2706, 14-29 June 2003.
  

• José Meseguer.
  Executable Computational Logics: Combining Formal Methods and Language Based System Design (PS).
  In Proceedings of First Intl. Conf. on Formal Methods and Models for Co-Design (MEMOCODE'03), Mont St. Michel, France, IEEE Computer Society, pages 3-9, June 2003.
  

• Steven Eker, José Meseguer and Ambarish Sridharanarayanan.
  The Maude LTL Model Checker (PS).
  In Proceedings of 4th International Workshop on Rewriting Logic and its Applications (WRLA'02) Portland, Oregon, May 2003.
  

• Steven Eker, José Meseguer and Ambarish Sridharanarayanan.
  The Maude LTL Model Checker and its Implementation (PS).
  In 10th International SPIN Workshop on Model Checking of Software, May 2003.

• José Meseguer.
  Software Specification and Verification in Rewriting Logic (PS).
  Lectures at the Marktoberdorf International Summer School, Germany, 2002.

Maude Extensions and Formal Analysis Tools

• Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché and Xavier Urbain.
  Proving Termination of Membership Equational Programs (PS).
  In Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, Verona, Italy, 24-25 August 2004. ISBN 1-58113-835-0.
  

• Peter C. Ölveczky and José Meseguer.
  The Real-Time Maude 2.0 System (PS).
  In Proceedings of the FASE'04, Barcelona, Spain, Springer-Verlag LNCS, March-April 2004.

• Peter C. Ölveczky and José Meseguer.
  Specification and Analysis of Real-Time Systems Using Real-Time Maude. (PS).
  In Proceedings of 6th International Conference on Fundamental Approaches to Software Engineering (FASE 2003), Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - 31, Springer-Verlag LNCS, 2004.
  

• Peter C. Ölveczky and José Meseguer.
  Real-Time Maude 2.0 (PS).
  In Proceedings of 5th International Workshop on Rewriting Logic and its Applications (WRLA' 2004), Barcelona, Spain, March 27 - 28, Electronic Notes in Theoretical Computer Science, Elsevier, 2004.

• Narciso Martí-Oliet, José Meseguer and Alberto Verdejo.
  Towards a Strategy Language for Maude (PS).
  In Proceedings of the WRLA'04, Barcelona, Spain, Elsevier ENTCS, March 2004.
  

• José Meseguer, Nirman Kumar, Kaushik Sen and Gul Agha.
  A Rewriting Based Model of Probabilistic Distributed Object Systems (PS).
  In Proceedings of Formal Methods for Open Object-Based Distributed Systems (FMOODS 2003), Springer-Verlag LNCS, Vol. 2884, pages 32-46, 2003.

Programming Language Semantics and Analysis Tools

• José Meseguer, Azadeh Farzan, Feng Cheng and Grigore Rosu.
  Formal Analysis of Java Programs in JavaFAN (PS).
  In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), Boston, Mass., July 2004, Springer-Verlag LNCS, Vol. 3114, pages 510-505, 2004.
  

• Azadeh Farzan, José Meseguer and Grigore Rosu.
  Formal JVM Code Analysis in JavaFAN (PS).
  In Proceedings of AMAST'04, Stirling, Scotland, Springer-Verlag LNCS, Vol. 3116, pages 132-147, July 2004.
  

• José Meseguer and Christiano Braga.
  Modular Rewriting Semantics of Programming Languages.
  In Proceedings of AMAST'04, Stirling, Scotland, Springer-Verlag LNCS, Vol. 3116, pages 364-378, July 2004.

• José Meseguer and Grigore Rosu.
  Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools (PS).
  in Proceedings of the IJCAR'04, Cork, Ireland, Springer-Verlag LNCS, Vol. 3097, pages 1-44, July 2004.
  

• José Meseguer and Christiano Braga.
  Modular Rewriting Semantics in Practice (PS).
  In Proceedings of WRLA'04, Barcelona, Spain, Elsevier ENTCS, March 2004.

• Christiano Braga, E. Hermann Haeusler, José Meseguer and Peter Mosses.
  Mapping Modular SOS to Rewriting Logic.
  In Logic Based Program Synthesis and Transformation, 12th International Workshop LOPSTR 2002, Madrid, Spain, Springer-Verlag, LNCS, Vol. 2664, pages 262, September 2002.

Formal Specification of Middleware

• Sebastian Gutierrez-Nolasco, Nalini Venkatasubramanian, Mark-Oliver Stehr and Carolyn Talcott.
  A Formal Methods Approach to Adaptive Secure Group Communication.
  Submitted for Publication, 2004.

• Sebastian Gutierrez-Nolasco, Nalini Venkatasubramanian, Mark-Oliver Stehr and Carolyn Talcott.
  Exploring Adaptability of Secure Group Communication using Formal Prototyping Techniques.
  3rd Workshop on Adaptive and Reflective Middleware, October 2004.

• José Meseguer and Carolyn Talcott.
  Semantic Models for Distributed Object Reflection (PS).
  In Proceedings of 16th European Conference on Object-Oriented Programming, ECOOP 2002, Málaga, Spain, June 2002.

Foundations and Tools for Security Protocol Specification and Analysis

• Iliano Cervesato, Mark-Oliver Stehr.
  Representing the MSR Cryptoprotocol Specification Language in an Extension of Rewriting Logic with Dependent Types.
  In Proceedings of Fifth International Workshop on Rewriting Logic and its Applications (WRLA'2004) Barcelona, Spain, March 27-28 2004, Electronic Notes in Theoretical Computer Science, Elsevier, 2004.

• José Meseguer and Prasanna Thati.
  Symbolic Reachability Analysis Using Narrowing and its Application to Analysis of Cryptographic Protocols (PS).
  In Fifth International Workshop on Rewriting Logic and its Applications (WRLA). Electronic Notes in Theoretical Computer Science, Elsevier, 2004.