Automata in semimodule categories. - José Meseguer 001; Ignacio Sols (Category Theory Applied to Computation and Control, 1974)

On Order-Complete Universal Algebra and Enriched Functorial Semantics. - José Meseguer 001 (FCT, 1977)

Correctness of Recursive Flow Diagram Programs. - Joseph A. Goguen; José Meseguer 001 (MFCS, 1977)

A Birkhoff-Like Theorem for Algebraic Classes of Interpretations of Program Schemes. - José Meseguer 001 (ICFPC, 1981)

Universal Realization, Persistent Interconnection and Implementation of Abstract Modules. - Joseph A. Goguen; José Meseguer 001 (ICALP, 1982)

Finding Safe Paths in a Faulty Environment. - Danny Dolev; José Meseguer 001; Marshall C. Pease (PODC, 1982)

Rapid prototyping: in the OBJ executable specification language. - Joseph A. Goguen; José Meseguer 001 (Rapid Prototyping, 1982)

Security Policies and Security Models. - Joseph A. Goguen; José Meseguer 001 (S&P, 1982)

Completeness of many-sorted equational logic. - Joseph A. Goguen; José Meseguer 001 (ACM SIGPLAN Notices, 1982)

Correctness of Recursive Parallel Nondeterministic Flow Programs. - Joseph A. Goguen; José Meseguer 001 (J. Comput. Syst. Sci., 1983)

Equality, Types, Modules and Generics for Logic Programming. - Joseph A. Goguen; José Meseguer 001 (ICLP, 1984)

Unwinding and Inference Control. - Joseph A. Goguen; José Meseguer 001 (S&P, 1984)

Equality, Types, Modules, and (Why not ?) Generics for Logic Programming. - Joseph A. Goguen; José Meseguer 001 (J. Log. Program., 1984)

Operational Semantics for Order-Sorted Algebra. - Joseph A. Goguen; Jean-Pierre Jouannaud; José Meseguer 001 (ICALP, 1985)

Principles of OBJ2. - Kokichi Futatsugi; Joseph A. Goguen; Jean-Pierre Jouannaud; José Meseguer 001 (POPL, 1985)

EQLOG: Equality, Types, and Generic Modules For Logic Programming. - Joseph A. Goguen; José Meseguer 001 (Logic Programming: Functions, Relations, and Equations, 1986)

Concurrent term rewriting as a model of computation. - Joseph A. Goguen; Claude Kirchner; José Meseguer 001 (Graph Reduction, 1986)

Remarks on remarks on many-sorted algebras with possibly emtpay carrier sets. - Joseph A. Goguen; José Meseguer 001 (Bull. EATCS, 1986)

Extensions and foundations of object-oriented programming. - Joseph A. Goguen; José Meseguer 001 (OOPWORK, 1986)

Foundations and extensions of object-oriented programming (abstract only). - Joseph A. Goguen; José Meseguer 001 (OOPWORK, 1986)

Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics. - Joseph A. Goguen; José Meseguer 001 (Research Directions in Object-Oriented Programming, 1987)

An Introduction to OBJ 3. - Joseph A. Goguen; Claude Kirchner; Hélène Kirchner; Aristide Mégrelis; José Meseguer 001; Timothy C. Winkler (CTRS, 1987)

Parameterized Programming in OBJ2. - Kokichi Futatsugi; Joseph A. Goguen; José Meseguer 001; Koji Okada (ICSE, 1987)

Order-Sorted Algebra solves the Constructor-Selector, Multiple - Joseph A. Goguen; José Meseguer 001 (LICS, 1987)

Models and Equality for Logical Programming. - Joseph A. Goguen; José Meseguer 001 (TAPSOFT, Vol.1, 1987)

On the Axiomatization of "If-Then-Else". - Irène Guessarian; José Meseguer 001 (SIAM J. Comput., 1987)

Remarks on Remarks on Many-Sorted Equational Logic. - Joseph A. Goguen; José Meseguer 001 (ACM SIGPLAN Notices, 1987)

Software for the Rewrite Rule Machine. - Joseph A. Goguen; José Meseguer 001 (FGCS, 1988)

Operational Semantics of OBJ-3 (Extended Abstract). - Claude Kirchner; Hélène Kirchner; José Meseguer 001 (ICALP, 1988)

Petri Nets Are Monoids: A New Algebraic Foundation for Net Theory - José Meseguer 001; Ugo Montanari (LICS, 1988)

Axiomatizing Net Computations and Processes - Pierpaolo Degano; José Meseguer 001; Ugo Montanari (LICS, 1989)

Relating Models of Polymorphism. - José Meseguer 001 (POPL, 1989)

Order-Sorted Unification. - José Meseguer 001; Joseph A. Goguen (J. Symb. Comput., 1989)

Compiling Concurrent Rewriting onto the Rewrite Rule Machine. - Hitoshi Aida; Joseph A. Goguen; José Meseguer 001 (CTRS, 1990)

Conditional Rewriting Logic: Deduction, Models and Concurrency. - José Meseguer 001 (CTRS, 1990)

A Logical Theory of Concurrent Objects. - José Meseguer 001 (OOPSLA/ECOOP, 1990)

Rewriting as a unified model of concurrency. - José Meseguer 001 (OOPSLA/ECOOP Workshop on Object-based Concurrent Programming, 1990)

Petri Nets Are Monoids - José Meseguer 001; Ugo Montanari (Inf. Comput., 1990)

Parallel Programmming in Maude. - José Meseguer 001; Timothy C. Winkler (Research Directions in High-Level Parallel Programming Languages, 1991)

From Petri Nets to Linear Logic through Categories: A Survey. - Narciso Martí-Oliet; José Meseguer 001 (Int. J. Found. Comput. Sci., 1991)

Temporal Structures. - Ross Casley; Roger F. Crew; José Meseguer 001; Vaughan R. Pratt (Math. Struct. Comput. Sci., 1991)

From Petri Nets to Linear Logic. - Narciso Martí-Oliet; José Meseguer 001 (Math. Struct. Comput. Sci., 1991)

Multiparadigm Logic Programming. - José Meseguer 001 (ALP, 1992)

On the Semantics of Petri Nets. - José Meseguer 001; Ugo Montanari; Vladimiro Sassone (CONCUR, 1992)

Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. - Joseph A. Goguen; José Meseguer 001 (Theor. Comput. Sci., 1992)

Conditioned Rewriting Logic as a United Model of Concurrency. - José Meseguer 001 (Theor. Comput. Sci., 1992)

Final Algebras, Cosemicomputable Algebras and Degrees of Unsolvability. - Lawrence S. Moss; José Meseguer 001; Joseph A. Goguen (Theor. Comput. Sci., 1992)

Solving the Inheritance Anomaly in Concurrent Object-Oriented Programming. - José Meseguer 001 (ECOOP, 1993)

May I Borrow Your Logic? - Maura Cerioli; José Meseguer 001 (MFCS, 1993)

A Logical Semantics for Object-Oriented Databases. - José Meseguer 001; Xiaolei Qian (SIGMOD Conference, 1993)

Order-Sorted Algebra Solves the Constructor-Selector, Multiple Representation, and Coercion Problems - José Meseguer 001; Joseph A. Goguen (Inf. Comput., 1993)

On the Model of Computation of Place/Transition Petri Nets. - José Meseguer 001; Ugo Montanari; Vladimiro Sassone (Application and Theory of Petri Nets, 1994)

From Abstract Data Types to Logical Frameworks. - José Meseguer 001; Narciso Martí-Oliet (COMPASS/ADT, 1994)

The Rewrite Rule Machine Node Architecture and Its Performance. - Patrick Lincoln; José Meseguer 001; Livio Ricciulli (CONPAR, 1994)

Specification, Transformation, and Programming of Concurrent Systems in Rewriting Logic. - Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001 (Specification of Parallel Algorithms, 1994)

Compiling Rewriting onto SIMD and MIMD/SIMD Maschines. - Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Livio Ricciulli (PARLE, 1994)

Distributed Simulation of Parallel Executions. - Livio Ricciulli; Patrick Lincoln; José Meseguer 001 (Annual Simulation Symposium, 1996)

Rewriting Logic as a Semantic Framework for Concurrency: a Progress Report. - José Meseguer 001 (CONCUR, 1996)

Axiomatizing the Algebra of Net Computations and Processes. - Pierpaolo Degano; José Meseguer 001; Ugo Montanari (Acta Informatica, 1996)

Why OOP Needs New Semantic Foundations. - José Meseguer 001 (ACM Comput. Surv., 1996)

Principles of Maude. - Manuel Clavel; Steven Eker; Patrick Lincoln; José Meseguer 001 (WRLA, 1996)

Reflection and strategies in rewriting logic. - Manuel Clavel; José Meseguer 001 (WRLA, 1996)

Rewriting logic as a logical and semantic framework. - Narciso Martí-Oliet; José Meseguer 001 (WRLA, 1996)

Preface. - José Meseguer 001 (WRLA, 1996)

Specifying real-time systems in rewriting logic. - Peter Csaba Ölveczky; José Meseguer 001 (WRLA, 1996)

Software Component Search. - Joseph A. Goguen; Doan Nguyen; José Meseguer 001; Luqi; Du Zhang; Valdis Berzins (J. Syst. Integr., 1996)

Inclusions and Subtypes I: First-Order Case. - Narciso Martí-Oliet; José Meseguer 001 (J. Log. Comput., 1996)

Inclusions and Subtypes II: Higher-Order Case. - Narciso Martí-Oliet; José Meseguer 001 (J. Log. Comput., 1996)

Process versus Unfolding Semantics for Place/Transition Petri Nets. - José Meseguer 001; Ugo Montanari; Vladimiro Sassone (Theor. Comput. Sci., 1996)

Representation Theorems for Petri Nets. - José Meseguer 001; Ugo Montanari; Vladimiro Sassone (Foundations of Computer Science: Potential - Theory - Cognition, 1997)

Membership algebra as a logical framework for equational specification. - José Meseguer 001 (WADT, 1997)

Mapping tile logic into rewriting logic. - José Meseguer 001; Ugo Montanari (WADT, 1997)

On the Semantics of Place/Transition Petri Nets. - José Meseguer 001; Ugo Montanari; Vladimiro Sassone (Math. Struct. Comput. Sci., 1997)

May I Borrow Your Logic? (Transporting Logical Structures Along Maps). - Maura Cerioli; José Meseguer 001 (Theor. Comput. Sci., 1997)

A Comparison of Petri Net Semantics under the Collective Token Philosophy. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari; Vladimiro Sassone (ASIAN, 1998)

On the Semantics of GAEA. - Hiroshi Ishikawa 001; Takuo Watanabe; Kokichi Futatsugi; José Meseguer 001; Hideyuki Nakashima (Fuji International Symposium on Functional and Logic Programming, 1998)

A Logical Framework for Distributed Systems and Communication Protocols. - José Meseguer 001 (FORTE, 1998)

Internal strategies in a rewriting implementation of tile systems. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari (WRLA, 1998)

Metalevel computation in Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001 (WRLA, 1998)

Maude as a metalanguage. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Jose F. Quesada (WRLA, 1998)

An extensible module algebra for Maude. - Francisco Durán 001; José Meseguer 001 (WRLA, 1998)

Mapping OMRS to rewriting logic. - José Meseguer 001; Carolyn L. Talcott (WRLA, 1998)

A Partial Order Event Model for Concurrent Objects. - José Meseguer 001; Carolyn L. Talcott (CONCUR, 1999)

Executable Tile Specifications for Process Calculi. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari (FASE, 1999)

Maude as a Formal Meta-tool. - Manuel Clavel; Francisco Durán 001; Steven Eker; José Meseguer 001; Mark-Oliver Stehr (World Congress on Formal Methods, 1999)

The Maude System. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Jose F. Quesada (RTA, 1999)

Towards a Verification Logic for Rewriting Logic. - José Luiz Fiadeiro; T. S. E. Maibaum; Narciso Martí-Oliet; José Meseguer 001; Isabel Pita (WADT, 1999)

Functorial semantics for Petri nets under the individual token philosophy. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari; Vladimiro Sassone (CTCS, 1999)

Structured Theories and Institutions. - Francisco Durán 001; José Meseguer 001 (CTCS, 1999)

Maude Action Tool: Using Reflection to Map Action Semantics to Rewriting Logic. - Christiano de Oliveira Braga; Edward Hermann Haeusler; José Meseguer 001; Peter D. Mosses (AMAST, 2000)

Using Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Jose F. Quesada (FASE, 2000)

Rewriting Logic and Maude: a Wide-Spectrum Semantic Framework for Object-Based Distributed Systems. - José Meseguer 001 (FMOODS, 2000)

Composing and Controlling Search in Reasoning Theories Using Mappings. - Alessandro Coglio; Fausto Giunchiglia; José Meseguer 001; Carolyn L. Talcott (FroCoS, 2000)

Rewriting Logic as a Metalogical Framework. - David A. Basin; Manuel Clavel; José Meseguer 001 (FSTTCS, 2000)

Specification and Formal Analysis of a PLAN Algorithm in Maude. - Bow-Yaw Wang; José Meseguer 001; Carl A. Gunter (ICDCS Workshop on Distributed System Validation and Verification, 2000)

Principles of Mobile Maude. - Francisco Durán 001; Steven Eker; Patrick Lincoln; José Meseguer 001 (ASA/MA, 2000)

Rewriting Logic and Maude: Concepts and Applications. - José Meseguer 001 (RTA, 2000)

Towards Maude 2.0. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Jose F. Quesada (WRLA, 2000)

Rewriting Semantics of Meta-Objects and Composable Distributed Services. - Grit Denker; José Meseguer 001; Carolyn L. Talcott (WRLA, 2000)

Parameterized Theories and Views in Full Maude 2.0. - Francisco Durán 001; José Meseguer 001 (WRLA, 2000)

Real-Time Maude: A Tool for Simulating and Analyzing Real-Time and Hybrid Systems. - Peter Csaba Ölveczky; José Meseguer 001 (WRLA, 2000)

Maude. - José Meseguer 001; Carolyn L. Talcott (ACM SIGSOFT Softw. Eng. Notes, 2000)

Semantic interoperation of open systems. - José Meseguer 001; Carolyn L. Talcott (ACM SIGSOFT Softw. Eng. Notes, 2000)

Specification and proof in membership equational logic. - Adel Bouhoula; Jean-Pierre Jouannaud; José Meseguer 001 (Theor. Comput. Sci., 2000)

Rewriting Logic as a Unifying Framework for Petri Nets. - Mark-Oliver Stehr; José Meseguer 001; Peter Csaba Ölveczky (Unifying Petri Nets, 2001)

Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude. - Peter Csaba Ölveczky; Mark Keaton; José Meseguer 001; Carolyn L. Talcott; Steve Zabele (FASE, 2001)

The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability). - Pavel Naumov; Mark-Oliver Stehr; José Meseguer 001 (TPHOLs, 2001)

Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework. - Mark-Oliver Stehr; José Meseguer 001; Peter Csaba Ölveczky (UNIGRA, 2001)

Functorial Models for Petri Nets. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari; Vladimiro Sassone (Inf. Comput., 2001)

Report on ETAPS 2000. - José Meseguer 001 (ACM SIGSOFT Softw. Eng. Notes, 2001)

Maude as a Wide-Spectrum Framework for Formal Modeling and Analysis of Active Networks. - José Meseguer 001; Peter Csaba Ölveczky; Mark-Oliver Stehr; Carolyn L. Talcott (DANCE, 2002)

Semantic Models for Distributed Object Reflection. - José Meseguer 001; Carolyn L. Talcott (ECOOP, 2002)

A Total Approach to Partial Algebraic Specification. - José Meseguer 001; Grigore Rosu (ICALP, 2002)

Mapping Modular SOS to Rewriting Logic. - Christiano de Oliveira Braga; Edward Hermann Haeusler; José Meseguer 001; Peter D. Mosses (LOPSTR, 2002)

Pathway Logic: Symbolic Analysis of Biological Signaling. - Steven Eker; Merrill Knapp; Keith Laderoute; Patrick Lincoln; José Meseguer 001; M. Kemal Sönmez (Pacific Symposium on Biocomputing, 2002)

Tiling Transactions in Rewriting Logic. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari (WRLA, 2002)

The Maude LTL Model Checker. - Steven Eker; José Meseguer 001; Ambarish Sridharanarayanan (WRLA, 2002)

Towards Behavioral Maude: Behavioral Membership Equational Logic. - José Meseguer 001; Grigore Rosu (CMCS, 2002)

Symmetric Monoidal and Cartesian Double Categories as a Semantic Framework for Tile Logic. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari (Math. Struct. Comput. Sci., 2002)

Maude: specification and programming in rewriting logic. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Jose F. Quesada (Theor. Comput. Sci., 2002)

Reflection in conditional rewriting logic. - Manuel Clavel; José Meseguer 001 (Theor. Comput. Sci., 2002)

Rewriting logic: roadmap and bibliography. - Narciso Martí-Oliet; José Meseguer 001 (Theor. Comput. Sci., 2002)

Preface. - Narciso Martí-Oliet; José Meseguer 001 (Theor. Comput. Sci., 2002)

Specification of real-time and hybrid systems in rewriting logic. - Peter Csaba Ölveczky; José Meseguer 001 (Theor. Comput. Sci., 2002)

Certifying and Synthesizing Membership Equational Proofs. - Grigore Rosu; Steven Eker; Patrick Lincoln; José Meseguer 001 (FME, 2003)

A Rewriting Based Model for Probabilistic Distributed Object Systems. - Nirman Kumar; Koushik Sen; José Meseguer 001; Gul Agha (FMOODS, 2003)

Generalized Rewrite Theories. - Roberto Bruni 001; José Meseguer 001 (ICALP, 2003)

Algebraic Theories for Contextual Pre-nets. - Roberto Bruni 001; José Meseguer 001; Ugo Montanari; Vladimiro Sassone (ICTCS, 2003)

Executable Computational Logics: Combining Formal Methods and Programming Language Based System Design. - José Meseguer 001 (MEMOCODE, 2003)

The Maude 2.0 System. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (RTA, 2003)

The Maude LTL Model Checker and Its Implementation. - Steven Eker; José Meseguer 001; Ambarish Sridharanarayanan (SPIN, 2003)

Formal JVM Code Analysis in JavaFAN. - Azadeh Farzan; José Meseguer 001; Grigore Rosu (AMAST, 2004)

Modular Rewriting Semantics of Programming Languages. - José Meseguer 001; Christiano Braga (AMAST, 2004)

Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework. - Mark-Oliver Stehr; José Meseguer 001 (Essays in Memory of Ole-Johan Dahl, 2004)

Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. - José Meseguer 001; Grigore Rosu (IJCAR, 2004)

Formal Analysis of Java Programs in JavaFAN. - Azadeh Farzan; Feng Chen 006; José Meseguer 001; Grigore Rosu (CAV, 2004)

Specification and Analysis of Real-Time Systems Using Real-Time Maude. - Peter Csaba Ölveczky; José Meseguer 001 (FASE, 2004)

Natural Rewriting for General Term Rewriting Systems. - Santiago Escobar 001; José Meseguer 001; Prasanna Thati (LOPSTR, 2004)

Proving termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; José Meseguer 001; Claude Marché; Xavier Urbain (PEPM, 2004)

Theoroidal Maps as Algebraic Simulations. - Narciso Martí-Oliet; José Meseguer 001; Miguel Palomino (WADT, 2004)

Modular Rewriting Semantics in Practice. - Christiano Braga; José Meseguer 001 (WRLA, 2004)

Towards a Strategy Language for Maude. - Narciso Martí-Oliet; José Meseguer 001; Alberto Verdejo (WRLA, 2004)

Real-Time Maude 2.1. - Peter Csaba Ölveczky; José Meseguer 001 (WRLA, 2004)

Reflective metalogical frameworks. - David A. Basin; Manuel Clavel; José Meseguer 001 (ACM Trans. Comput. Log., 2004)

Functorial Semantics of Rewrite Theories. - José Meseguer 001 (Formal Methods in Software and Systems Modeling, 2005)

A Categorical Approach to Simulations. - Miguel Palomino; José Meseguer 001; Narciso Martí-Oliet (CALCO, 2005)

A rewriting-based inference system for the NRL protocol analyzer: grammar generation. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (FMSE, 2005)

A Rewriting Logic Sampler. - José Meseguer 001 (ICTAC, 2005)

Termination of Fair Computations in Term Rewriting. - Salvador Lucas; José Meseguer 001 (LPAR, 2005)

Natural Narrowing for General Term Rewriting Systems. - Santiago Escobar 001; José Meseguer 001; Prasanna Thati (RTA, 2005)

A Sufficient Completeness Reasoning Tool for Partial Specifications. - Joe Hendrix; Manuel Clavel; José Meseguer 001 (RTA, 2005)

Localized Fairness: A Rewriting Semantics. - José Meseguer 001 (RTA, 2005)

Computational Logical Frameworks and Generic Program Analysis Technologies. - José Meseguer 001; Grigore Rosu (VSTTE, 2005)

PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. - Gul A. Agha; José Meseguer 001; Koushik Sen (QAPL, 2005)

Operational termination of conditional term rewriting systems. - Salvador Lucas; Claude Marché; José Meseguer 001 (Inf. Process. Lett., 2005)

A Verification Logic for Rewriting Logic. - Narciso Martí-Oliet; Isabel Pita; José Luiz Fiadeiro; José Meseguer 001; T. S. E. Maibaum (J. Log. Comput., 2005)

State Space Reduction of Rewrite Theories Using Invisible Transitions. - Azadeh Farzan; José Meseguer 001 (AMAST, 2006)

From OBJ to Maude and Beyond. - José Meseguer 001 (Essays Dedicated to Joseph A. Goguen, 2006)

A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. - Joe Hendrix; José Meseguer 001; Hitoshi Ohsaki (IJCAR, 2006)

Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems. - José Meseguer 001; Raman Sharykin (HSCC, 2006)

Joseph Goguen (1941-2006). - Kokichi Futatsugi; Jean-Pierre Jouannaud; José Meseguer 001 (Bull. EATCS, 2006)

Deduction, Strategies, and Rewriting. - Steven Eker; Narciso Martí-Oliet; José Meseguer 001; Alberto Verdejo (STRATEGIES@IJCAR, 2006)

Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (SecReT@ICALP, 2006)

Narrowing and Rewriting Logic: from Foundations to Applications. - Santiago Escobar 001; José Meseguer 001; Prasanna Thati (WFLP, 2006)

Partial Order Reduction for Rewriting Semantics of Programming Languages. - Azadeh Farzan; José Meseguer 001 (WRLA, 2006)

A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis. - Michael Katelman; José Meseguer 001 (WRLA, 2006)

Recent Advances in Real-Time Maude. - Peter Csaba Ölveczky; José Meseguer 001 (RULE@FLoC, 2006)

Abstraction and Completeness for Real-Time Maude. - Peter Csaba Ölveczky; José Meseguer 001 (WRLA, 2006)

Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics. - Ralf Sasse; José Meseguer 001 (WRLA, 2006)

Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. - Peter Csaba Ölveczky; José Meseguer 001; Carolyn L. Talcott (Formal Methods Syst. Des., 2006)

Semantic foundations for generalized rewrite theories. - Roberto Bruni 001; José Meseguer 001 (Theor. Comput. Sci., 2006)

A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (Theor. Comput. Sci., 2006)

Complete symbolic reachability analysis using back-and-forth narrowing. - Prasanna Thati; José Meseguer 001 (Theor. Comput. Sci., 2006)

The Maude Formal Tool Environment. - Manuel Clavel; Francisco Durán 001; Joe Hendrix; Salvador Lucas; José Meseguer 001; Peter Csaba Ölveczky (CALCO, 2007)

Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (FOSAD, 2007)

Introduction. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Using Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Syntax and Basic Parsing. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Functional Modules. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

A Hierarchy of Data Types: From Trees to Sets. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

System Modules. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Module Operations. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Predefined Data Modules. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Object-Based Programming. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Model Checking Invariants Through Search. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

LTL Model Checking. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Reflection, Metalevel Computation, and Strategies. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Metaprogramming Applications. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

User Interfaces and Metalanguage Applications. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Full Maude: Extending Core Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Object-Oriented Modules. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

A Sampler of Application Areas. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Debugging and Troubleshooting. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Complete List of Maude Commands. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Core Maude Grammar. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (All About Maude, 2007)

Some Tools. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott; Christiano Braga; Azadeh Farzan; Joe Hendrix; Peter Csaba Ölveczky; Miguel Palomino; et al. (All About Maude, 2007)

Playing with Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott; Miguel Palomino; Alberto Verdejo (All About Maude, 2007)

Specifying Parameterized Data Structures in Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott; Miguel Palomino; Alberto Verdejo (All About Maude, 2007)

Mobile Maude. - Manuel Clavel; Francisco Durán 001; Steven Eker; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott; Adrián Riesco 001; Alberto Verdejo (All About Maude, 2007)

Real-time rewriting semantics of orc. - Musab AlTurki; José Meseguer 001 (PPDP, 2007)

Symbolic Model Checking of Infinite-State Systems Using Narrowing. - Santiago Escobar 001; José Meseguer 001 (RTA, 2007)

On the Completeness of Context-Sensitive Order-Sorted Specifications. - Joe Hendrix; José Meseguer 001 (RTA, 2007)

A Systematic Approach to Uncover Security Flaws in GUI Logic. - José Meseguer 001; Ralf Sasse; Helen J. Wang; Yi-Min Wang (S&P, 2007)

Reduction Semantics and Formal Analysis of Orc Programs. - Musab AlTurki; José Meseguer 001 (WWV, 2007)

Algebraic Stuttering Simulations. - Narciso Martí-Oliet; José Meseguer 001; Miguel Palomino (PROLE, 2007)

A Rewriting Logic Approach to Operational Semantics (Extended Abstract). - Traian-Florin Serbanuta; Grigore Rosu; José Meseguer 001 (SOS@LICS/ICALP, 2007)

Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. - José Meseguer 001; Prasanna Thati (High. Order Symb. Comput., 2007)

Semantics and pragmatics of Real-Time Maude. - Peter Csaba Ölveczky; José Meseguer 001 (High. Order Symb. Comput., 2007)

A Rewriting Decision Procedure for Dijkstra-Scholten's Syllogistic Logic with Complements. - Camilo Rocha; José Meseguer 001 (Rev. Colomb. de Computación, 2007)

Maude's module algebra. - Francisco Durán 001; José Meseguer 001 (Sci. Comput. Program., 2007)

Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. - Manuel Clavel; José Meseguer 001; Miguel Palomino (Theor. Comput. Sci., 2007)

The rewriting logic semantics project. - José Meseguer 001; Grigore Rosu (Theor. Comput. Sci., 2007)

Theorem Proving Modulo Based on Boolean Equational Procedures. - Camilo Rocha; José Meseguer 001 (RelMiCS, 2008)

The Temporal Logic of Rewriting: A Gentle Introduction. - José Meseguer 001 (Concurrency, Graphs and Models, 2008)

Ugo Montanari in a Nutshell. - Rocco De Nicola; Pierpaolo Degano; José Meseguer 001 (Concurrency, Graphs and Models, 2008)

MTT: The Maude Termination Tool (System Description). - Francisco Durán 001; Salvador Lucas; José Meseguer 001 (IJCAR, 2008)

State Space Reduction in the Maude-NRL Protocol Analyzer. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (ESORICS, 2008)

Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers. - Rohit Chadha; Carl A. Gunter; José Meseguer 001; Ravinder Shankesi; Mahesh Viswanathan 001 (FMOODS, 2008)

Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking. - Michael Katelman; José Meseguer 001; Jennifer C. Hou (FMOODS, 2008)

A Modular Equational Generalization Algorithm. - María Alpuente; Santiago Escobar 001; José Meseguer 001; Pedro Ojeda (LOPSTR, 2008)

Directed-Logical Testing for Functional Verification of Microprocessors. - Michael Katelman; José Meseguer 001; Santiago Escobar 001 (MEMOCODE, 2008)

Order-sorted dependency pairs. - Salvador Lucas; José Meseguer 001 (PPDP, 2008)

Effectively Checking the Finite Variant Property. - Santiago Escobar 001; José Meseguer 001; Ralf Sasse (RTA, 2008)

The Real-Time Maude Tool. - Peter Csaba Ölveczky; José Meseguer 001 (TACAS, 2008)

Equational Unification by Variant Narrowing (Extended Abstract). - Santiago Escobar 001; José Meseguer 001; Ralf Sasse (UNIF, 2008)

What Is a Multi-modeling Language? - Artur Boronat; Alexander Knapp; José Meseguer 001; Martin Wirsing (WADT, 2008)

Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol. - Musab AlTurki; José Meseguer 001; Carl A. Gunter (SecReT@LICS/CSF, 2008)

Order-Sorted Generalization. - María Alpuente; Santiago Escobar 001; José Meseguer 001; Pedro Ojeda (WFLP, 2008)

A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting. - Kyungmin Bae; José Meseguer 001 (RULE, 2008)

Methods for Proving Termination of Rewriting-based Programming Languages by Transformation. - Francisco Durán 001; Salvador Lucas; José Meseguer 001 (PROLE, 2008)

Web Services and Interoperability for the Maude Termination Tool. - Francisco Durán 001; Salvador Lucas; José Meseguer 001; Francisco Gutiérrez (PROLE, 2008)

Variant Narrowing and Equational Unification. - Santiago Escobar 001; José Meseguer 001; Ralf Sasse (WRLA, 2008)

Order-sorted Equational Unification Revisited. - Joe Hendrix; José Meseguer 001 (RULE, 2008)

Operational Termination of Membership Equational Programs: the Order-Sorted Way. - Salvador Lucas; José Meseguer 001 (WRLA, 2008)

A Rewriting Semantics for Maude Strategies. - Narciso Martí-Oliet; José Meseguer 001; Alberto Verdejo (WRLA, 2008)

Termination of just/fair computations in term rewriting. - Salvador Lucas; José Meseguer 001 (Inf. Comput., 2008)

Proving operational termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; Claude Marché; José Meseguer 001; Xavier Urbain (High. Order Symb. Comput., 2008)

Equational abstractions. - José Meseguer 001; Miguel Palomino; Narciso Martí-Oliet (Theor. Comput. Sci., 2008)

Design of Complex Cyber Physical Systems with Formalized Architectural Patterns. - Lui Sha; José Meseguer 001 (Software-Intensive Systems and New Computing Paradigms, 2008)

Order-Sorted Parameterization and Induction. - José Meseguer 001 (Semantics and Algebraic Specification, 2009)

Model-Checking DoS Amplification for VoIP Session Initiation. - Ravinder Shankesi; Musab AlTurki; Ralf Sasse; Carl A. Gunter; José Meseguer 001 (ESORICS, 2009)

Rewriting Logic Semantics and Verification of Model Transformations. - Artur Boronat; Reiko Heckel; José Meseguer 001 (FASE, 2009)

Termination Modulo Combinations of Equational Theories. - Francisco Durán 001; Salvador Lucas; José Meseguer 001 (FroCoS, 2009)

MOMENT2: EMF Model Transformations in Maude. - Artur Boronat; José Meseguer 001 (JISBD, 2009)

Unification and Narrowing in Maude 2.4. - Manuel Clavel; Francisco Durán 001; Steven Eker; Santiago Escobar 001; Patrick Lincoln; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (RTA, 2009)

Algebraic Semantics of OCL-Constrained Metamodel Specifications. - Artur Boronat; José Meseguer 001 (TOOLS (47), 2009)

A Graphical User Interface for Maude-NPA. - Sonia Santiago; Carolyn L. Talcott; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (PROLE, 2009)

A rewriting logic approach to operational semantics. - Traian-Florin Serbanuta; Grigore Rosu; José Meseguer 001 (Inf. Comput., 2009)

Sequential Protocol Composition in Maude-NPA. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (ESORICS, 2010)

Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. - Peter Csaba Ölveczky; Artur Boronat; José Meseguer 001 (FMOODS/FORTE, 2010)

vlogsl: A Strategy Language for Simulation-Based Verification of Hardware. - Michael Katelman; José Meseguer 001 (Haifa Verification Conference, 2010)

Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. - Joe Hendrix; Deepak Kapur; José Meseguer 001 (ITP, 2010)

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories. - Camilo Rocha; José Meseguer 001 (LPAR (Yogyakarta), 2010)

A formal executable semantics of Verilog. - Patrick O'Neil Meredith; Michael Katelman; José Meseguer 001; Grigore Rosu (MEMOCODE, 2010)

Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA. - Ralf Sasse; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (STM, 2010)

A Dependency Pair Framework for A OR C-Termination. - Beatriz Alarcón; Salvador Lucas; José Meseguer 001 (WRLA, 2010)

The Linear Temporal Logic of Rewriting Maude Model Checker. - Kyungmin Bae; José Meseguer 001 (WRLA, 2010)

A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications. - Francisco Durán 001; José Meseguer 001 (WRLA, 2010)

A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories. - Francisco Durán 001; José Meseguer 001 (WRLA, 2010)

Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits. - Michael Katelman; Sean Keller; José Meseguer 001 (WRLA, 2010)

A Formal Pattern Architecture for Safe Medical Systems. - Mu Sun; José Meseguer 001; Lui Sha (WRLA, 2010)

Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis - Musab AlTurki; José Meseguer 001 (RTRTS, 2010)

Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family - Peter Csaba Ölveczky; José Meseguer 001 (RTRTS, 2010)

Distributed Real-Time Emulation of Formally-Defined Patterns for Safe Medical Device Control - Mu Sun; José Meseguer 001 (RTRTS, 2010)

Using the PALS Architecture to Verify a Distributed Topology Control Protocol for Wireless Multi-Hop Networks in the Presence of Node Failures - Michael Katelman; José Meseguer 001 (RTRTS, 2010)

An algebraic semantics for MOF. - Artur Boronat; José Meseguer 001 (Formal Aspects Comput., 2010)

Algebraic simulations. - José Meseguer 001; Miguel Palomino; Narciso Martí-Oliet (J. Log. Algebraic Methods Program., 2010)

PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. - Musab AlTurki; José Meseguer 001 (CALCO, 2011)

Proving Safety Properties of Rewrite Theories. - Camilo Rocha; José Meseguer 001 (CALCO, 2011)

State/Event-Based LTL Model Checking under Parametric Generalized Fairness. - Kyungmin Bae; José Meseguer 001 (CAV, 2011)

Synchronous AADL and Its Formal Analysis in Real-Time Maude. - Kyungmin Bae; Peter Csaba Ölveczky; Abdullah Al-Nayeem; José Meseguer 001 (ICFEM, 2011)

Verification of microarchitectural refinements in rule-based systems. - Nirav Dave; Michael Katelman; Myron King; Arvind 001; José Meseguer 001 (MEMOCODE, 2011)

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. - Santiago Escobar 001; Deepak Kapur; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (PPDP, 2011)

Incremental checking of well-founded recursive specifications modulo axioms. - Felix Schernhammer; José Meseguer 001 (PPDP, 2011)

Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; José Meseguer 001; Carolyn L. Talcott (RTA, 2011)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (UNIF, 2011)

Automated Model Synchronization: A Case Study on UML with Maude. - Artur Boronat; José Meseguer 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Maude. - José Meseguer 001 (Encyclopedia of Parallel Computing, 2011)

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (ESORICS, 2012)

Formal Patterns for Multi-rate Distributed Real-Time Systems. - Kyungmin Bae; José Meseguer 001; Peter Csaba Ölveczky (FACS, 2012)

IBOS: A Correct-By-Construction Modular Browser. - Ralf Sasse; Samuel T. King; José Meseguer 001; Shuo Tang (FACS, 2012)

The SynchAADL2Maude Tool. - Kyungmin Bae; Peter Csaba Ölveczky; José Meseguer 001; Abdullah Al-Nayeem (FASE, 2012)

Stable Availability under Denial of Service Attacks through Formal Patterns. - Jonas Eckhardt; Tobias Mühlbauer; Musab AlTurki; José Meseguer 001; Martin Wirsing (FASE, 2012)

State Space c-Reductions of Concurrent Systems in Rewriting Logic. - Alberto Lluch-Lafuente; José Meseguer 001; Andrea Vandin (ICFEM, 2012)

Statistical Model Checking for Composite Actor Systems. - Jonas Eckhardt; Tobias Mühlbauer; José Meseguer 001; Martin Wirsing (WADT, 2012)

Model Checking LTLR Formulas under Localized Fairness. - Kyungmin Bae; José Meseguer 001 (WRLA, 2012)

Design and Analysis of Cloud-Based Architectures with KLAIM and Maude. - Martin Wirsing; Jonas Eckhardt; Tobias Mühlbauer; José Meseguer 001 (WRLA, 2012)

PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude - Kyungmin Bae; Joshua Krisiloff; José Meseguer 001; Peter Csaba Ölveczky (FTSCS, 2012)

On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. - Francisco Durán 001; José Meseguer 001 (J. Log. Algebraic Methods Program., 2012)

Folding variant narrowing and optimal variant termination. - Santiago Escobar 001; Ralf Sasse; José Meseguer 001 (J. Log. Algebraic Methods Program., 2012)

Rewriting semantics of production rule sets. - Michael Katelman; Sean Keller; José Meseguer 001 (J. Log. Algebraic Methods Program., 2012)

Twenty years of rewriting logic. - José Meseguer 001 (J. Log. Algebraic Methods Program., 2012)

Formalization and correctness of the PALS architectural pattern for distributed real-time systems. - José Meseguer 001; Peter Csaba Ölveczky (Theor. Comput. Sci., 2012)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (CADE, 2013)

Formal Analysis of Fault-tolerant Group Key Management Using ZooKeeper. - Stephen Skeirik; Rakesh B. Bobba; José Meseguer 001 (CCGRID, 2013)

Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. - Kyungmin Bae; Santiago Escobar 001; José Meseguer 001 (RTA, 2013)

The rewriting logic semantics project: A progress report. - José Meseguer 001; Grigore Rosu (Inf. Comput., 2013)

Models for Logics and Conditional Constraints in Automated Proofs of Termination. - Salvador Lucas; José Meseguer 001 (AISC, 2014)

Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool. - Camilo Rocha; José Meseguer 001 (Specification, Algebra, and Software, 2014)

Definition, Semantics, and Analysis of Multirate Synchronous AADL. - Kyungmin Bae; Peter Csaba Ölveczky; José Meseguer 001 (FM, 2014)

A rewriting-based forwards semantics for Maude-NPA. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (HotSoS, 2014)

Formal Modeling and Analysis of Cassandra in Maude. - Si Liu 003; Muntasir Raihan Rahman; Stephen Skeirik; Indranil Gupta; José Meseguer 001 (ICFEM, 2014)

ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance. - María Alpuente; Santiago Escobar 001; Javier Espert; José Meseguer 001 (JELIA, 2014)

Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems. - Salvador Lucas; José Meseguer 001; Raúl Gutiérrez (LOPSTR, 2014)

Proving Operational Termination of Declarative Programs in General Logics. - Salvador Lucas; José Meseguer 001 (PPDP, 2014)

Theories of Homomorphic Encryption, Unification, and the Finite Variant Property. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Paliath Narendran (PPDP, 2014)

Predicate Abstraction of Rewrite Theories. - Kyungmin Bae; José Meseguer 001 (RTA-TLCA, 2014)

Analysis of the IBM CCA Security API Protocols in Maude-NPA. - Antonio González-Burgueño; Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (SSR, 2014)

A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA. - Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (STM, 2014)

Extensible Symbolic System Analysis. - José Meseguer 001 (UNIF, 2014)

Infinite-State Model Checking of LTLR Formulas Using Narrowing. - Kyungmin Bae; José Meseguer 001 (WRLA, 2014)

A Framework for Mobile Ad hoc Networks in Real-Time Maude. - Si Liu 003; Peter Csaba Ölveczky; José Meseguer 001 (WRLA, 2014)

Strong and Weak Operational Termination of Order-Sorted Rewrite Theories. - Salvador Lucas; José Meseguer 001 (WRLA, 2014)

2D Dependency Pairs for Proving Operational Termination of CTRSs. - Salvador Lucas; José Meseguer 001 (WRLA, 2014)

Formal Specification of Button-Related Fault-Tolerance Micropatterns. - Mu Sun; José Meseguer 001 (WRLA, 2014)

A modular order-sorted equational generalization algorithm. - María Alpuente; Santiago Escobar 001; Javier Espert; José Meseguer 001 (Inf. Comput., 2014)

State space reduction in the Maude-NRL Protocol Analyzer. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (Inf. Comput., 2014)

Formal patterns for multirate distributed real-time systems. - Kyungmin Bae; José Meseguer 001; Peter Csaba Ölveczky (Sci. Comput. Program., 2014)

Taming distributed system complexity through formal patterns. - José Meseguer 001 (Sci. Comput. Program., 2014)

Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories. - Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (Programming Languages with Applications to Biology and Security, 2015)

Formal Analysis of Leader Election in MANETs Using Real-Time Maude. - Si Liu 003; Peter Csaba Ölveczky; José Meseguer 001 (Software, Services, and Systems, 2015)

Localized Operational Termination in General Logics. - Salvador Lucas; José Meseguer 001 (Software, Services, and Systems, 2015)

Analysis of the PKCS#11 API Using the Maude-NPA Tool. - Antonio González-Burgueño; Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (SSR, 2015)

Executable rewriting logic semantics of Orc and formal analysis of Orc programs. - Musab A. AlTurki; José Meseguer 001 (J. Log. Algebraic Methods Program., 2015)

Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study. - Kyungmin Bae; Joshua Krisiloff; José Meseguer 001; Peter Csaba Ölveczky (Sci. Comput. Program., 2015)

Model checking linear temporal logic of rewriting formulas under localized fairness. - Kyungmin Bae; José Meseguer 001 (Sci. Comput. Program., 2015)

Constrained narrowing for conditional equational theories modulo axioms. - Andrew Cholewa; Santiago Escobar 001; José Meseguer 001 (Sci. Comput. Program., 2015)

Semantics, distributed implementation, and formal analysis of KLAIM models in Maude. - Jonas Eckhardt; Tobias Mühlbauer; José Meseguer 001; Martin Wirsing (Sci. Comput. Program., 2015)

Order-sorted equality enrichments modulo axioms. - Raúl Gutiérrez; José Meseguer 001; Camilo Rocha (Sci. Comput. Program., 2015)

Built-in Variant Generation and Unification, and Their Applications in Maude 2.7. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (IJCAR, 2016)

Order-Sorted Rewriting and Congruence Closure. - José Meseguer 001 (FoSSaCS, 2016)

Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (LOPSTR, 2016)

Strand spaces with choice via a process algebra semantics. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Sonia Santiago (PPDP, 2016)

Formal modeling and analysis of RAMP transaction systems. - Si Liu 003; Peter Csaba Ölveczky; Muntasir Raihan Rahman; Jatin Ganhotra; Indranil Gupta; José Meseguer 001 (SAC, 2016)

Towards Generic Monitors for Object-Oriented Real-Time Maude Specifications. - Antonio Moreno-Delgado; Francisco Durán 001; José Meseguer 001 (WRLA, 2016)

Effective Sequential Protocol Composition in Maude-NPA. - Sonia Santiago; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (CoRR, 2016)

Modeling and analyzing mobile ad hoc networks in Real-Time Maude. - Si Liu 003; Peter Csaba Ölveczky; José Meseguer 001 (J. Log. Algebraic Methods Program., 2016)

Normal forms and normal theories in conditional rewriting. - Salvador Lucas; José Meseguer 001 (J. Log. Algebraic Methods Program., 2016)

Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking. - Si Liu 003; Peter Csaba Ölveczky; Jatin Ganhotra; Indranil Gupta; José Meseguer 001 (ICFEM, 2017)

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates. - Raúl Gutiérrez; José Meseguer 001 (LOPSTR, 2017)

Equational formulas and pattern operations in initial order-sorted algebras. - José Meseguer 001; Stephen Skeirik (Formal Aspects Comput., 2017)

Dependency pairs for proving termination properties of conditional term rewriting systems. - Salvador Lucas; José Meseguer 001 (J. Log. Algebraic Methods Program., 2017)

Rewriting modulo SMT and open system analysis. - Camilo Rocha; José Meseguer 001; César A. Muñoz (J. Log. Algebraic Methods Program., 2017)

Quantitative Analysis of Consistency in NoSQL Key-Value Stores. - Si Liu 003; Jatin Ganhotra; Muntasir Raihan Rahman; Son Nguyen; Indranil Gupta; José Meseguer 001 (Leibniz Trans. Embed. Syst., 2017)

Strict coherence of conditional rewriting modulo axioms. - José Meseguer 001 (Theor. Comput. Sci., 2017)

ROLA: A New Distributed Transaction Protocol and Its Formal Analysis. - Si Liu 003; Peter Csaba Ölveczky; Keshav Santhanam; Qi Wang 017; Indranil Gupta; José Meseguer 001 (FASE, 2018)

Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (LOPSTR, 2018)

Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA. - Antonio González-Burgueño; Damián Aparicio-Sánchez; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (LPAR, 2018)

Formal Design of Cloud Computing Systems in Maude. - José Meseguer 001 (SBMF, 2018)

Modular Verification of Sequential Composition for Private Channels in Maude-NPA. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (STM, 2018)

Symbolic Reasoning Methods in Rewriting Logic and Maude. - José Meseguer 001 (WoLLIC, 2018)

Associative Unification and Symbolic Reasoning Modulo Associativity in Maude. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Carolyn L. Talcott (WRLA@ETAPS, 2018)

Proving Ground Confluence of Equational Specifications Modulo Axioms. - Francisco Durán 001; José Meseguer 001; Camilo Rocha (WRLA@ETAPS, 2018)

Formal Modeling and Analysis of the Walter Transactional Data Store. - Si Liu 003; Peter Csaba Ölveczky; Qi Wang 017; José Meseguer 001 (WRLA@ETAPS, 2018)

Generalized Rewrite Theories and Coherence Completion. - José Meseguer 001 (WRLA@ETAPS, 2018)

The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors. - Salvador Lucas; José Meseguer 001; Raúl Gutiérrez (J. Comput. Syst. Sci., 2018)

Metalevel algorithms for variant satisfiability. - Stephen Skeirik; José Meseguer 001 (J. Log. Algebraic Methods Program., 2018)

Variant-based satisfiability in initial algebras. - José Meseguer 001 (Sci. Comput. Program., 2018)

Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method. - Santiago Escobar 001; José Meseguer 001 (Foundations of Security, Protocols, and Equational Reasoning, 2019)

ACUOS2: A High-Performance System for Modular ACU Generalization with Subtyping and Inheritance. - María Alpuente; Demis Ballis; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (JELIA, 2019)

Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. - Si Liu 003; Peter Csaba Ölveczky; Min Zhang 002; Qi Wang 017; José Meseguer 001 (TACAS (2), 2019)

Strand Spaces with Choice via a Process Algebra Semantics. - Fan Yang 090; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (CoRR, 2019)

Read atomic transactions with prevention of lost updates: ROLA and its formal analysis. - Si Liu 003; Peter Csaba Ölveczky; Qi Wang 017; Indranil Gupta; José Meseguer 001 (Formal Aspects Comput., 2019)

Protocol Analysis with Time. - Damián Aparicio-Sánchez; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Julia Sapiña (INDOCRYPT, 2020)

Symbolic Computation in Maude: Some Tapas. - José Meseguer 001 (LOPSTR, 2020)

Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs. - Si Liu 003; Atul Sandur; José Meseguer 001; Peter Csaba Ölveczky; Qi Wang 017 (NFM, 2020)

Variants in the Infinitary Unification Wonderland. - José Meseguer 001 (WRLA@ETAPS, 2020)

Variant Satisfiability of Parameterized Strings. - José Meseguer 001 (WRLA@ETAPS, 2020)

Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification. - José Meseguer 001; Stephen Skeirik (WRLA@ETAPS, 2020)

Verification of the IBOS Browser Security Properties in Reachability Logic. - Stephen Skeirik; José Meseguer 001; Camilo Rocha (WRLA@ETAPS, 2020)

Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (Fundam. Informaticae, 2020)

A Constructor-Based Reachability Logic for Rewrite Theories. - Stephen Skeirik; Andrei Stefanescu; José Meseguer 001 (Fundam. Informaticae, 2020)

The 2D Dependency Pair Framework for Conditional Rewrite Systems - Part II: Advanced Processors and Implementation Techniques. - Salvador Lucas; José Meseguer 001; Raúl Gutiérrez (J. Autom. Reason., 2020)

A partial evaluation framework for order-sorted equational programs modulo axioms. - María Alpuente; Angel Cuenca-Ortega; Santiago Escobar 001; José Meseguer 001 (J. Log. Algebraic Methods Program., 2020)

Programming and symbolic computation in Maude. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Rubén Rubio; Carolyn L. Talcott (J. Log. Algebraic Methods Program., 2020)

Ground confluence of order-sorted conditional specifications modulo axioms. - Francisco Durán 001; José Meseguer 001; Camilo Rocha (J. Log. Algebraic Methods Program., 2020)

Generalized rewrite theories, coherence completion, and symbolic methods. - José Meseguer 001 (J. Log. Algebraic Methods Program., 2020)

Protocol Analysis with Time and Space. - Damián Aparicio-Sánchez; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001; Julia Sapiña (Protocols, Strands, and Logic, 2021)

Building Correct-by-Construction Systems with Formal Patterns. - José Meseguer 001 (WADT, 2022)

Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description). - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Rubén Rubio; Carolyn L. Talcott (IJCAR, 2022)

An Efficient Canonical Narrowing Implementation for Protocol Analysis. - Raúl López-Rueda; Santiago Escobar 001; José Meseguer 001 (WRLA@ETAPS, 2022)

Checking Sufficient Completeness by Inductive Theorem Proving. - José Meseguer 001 (WRLA@ETAPS, 2022)

On Ground Convergence and Completeness of Conditional Equational Program Hierarchies. - José Meseguer 001; Stephen Skeirik (WRLA@ETAPS, 2022)

Order-sorted equational generalization algorithm revisited. - María Alpuente; Santiago Escobar 001; José Meseguer 001; Julia Sapiña (Ann. Math. Artif. Intell., 2022)

Bridging the semantic gap between qualitative and quantitative models of distributed systems. - Si Liu 003; José Meseguer 001; Peter Csaba Ölveczky; Min Zhang 002; David A. Basin (Proc. ACM Program. Lang., 2022)

Optimizing Maude Programs via Program Specialization. - María Alpuente; Demis Ballis; Santiago Escobar 001; José Meseguer 001; Julia Sapiña (Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems, 2023)

Protocol Dialects as Formal Patterns. - D. Galán; Víctor García; Santiago Escobar 001; Catherine A. Meadows; José Meseguer 001 (ESORICS (2), 2023)

The Maude strategy language. - Steven Eker; Narciso Martí-Oliet; José Meseguer 001; Rubén Rubio; Alberto Verdejo (J. Log. Algebraic Methods Program., 2023)

Variants and satisfiability in the infinitary unification wonderland. - José Meseguer 001 (J. Log. Algebraic Methods Program., 2023)

NuITP: An Inductive Theorem Prover for Equational Program Verification. - Francisco J. Durán; Santiago Escobar 001; José Meseguer 001; Julia Sapiña (PPDP, 2024)

Programming Open Distributed Systems in Maude. - Francisco Durán 001; Steven Eker; Santiago Escobar 001; Narciso Martí-Oliet; José Meseguer 001; Rubén Rubio; Carolyn L. Talcott (PPDP, 2024)

Verifying Invariants by Deductive Model Checking. - Kyungmin Bae; Santiago Escobar 001; Raúl López-Rueda; José Meseguer 001; Julia Sapiña (WRLA, 2024)

Equivalence, and Property Internalization and Preservation for Equational Programs. - José Meseguer 001 (WRLA, 2024)

Capturing System Designs with Formal Executable Specifications. - José Meseguer 001 (FASE, 2025)

Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. - José Meseguer 001 (J. Log. Algebraic Methods Program., 2025)

Protocol Dialects as Formal Patterns: A Composable Theory of Lingos - Technical report. - Víctor García; Santiago Escobar 001; Catherine Meadows 001; José Meseguer 001 (CoRR, 2025)