# José Meseguer

According to our database1, José Meseguer authored at least 361 papers between 1974 and 2019.

Collaborative distances:

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

2019
Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

$${\textsf {ACUOS}}^\mathbf {2}$$ : A High-Performance System for Modular ACU Generalization with Subtyping and Inheritance.
Proceedings of the Logics in Artificial Intelligence - 16th European Conference, 2019

Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method.
Proceedings of the Foundations of Security, Protocols, and Equational Reasoning, 2019

2018
The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors.
J. Comput. Syst. Sci., 2018

Generalized Rewrite Theories and Coherence Completion.
Proceedings of the Rewriting Logic and Its Applications - 12th International Workshop, 2018

Formal Modeling and Analysis of the Walter Transactional Data Store.
Proceedings of the Rewriting Logic and Its Applications - 12th International Workshop, 2018

Proving Ground Confluence of Equational Specifications Modulo Axioms.
Proceedings of the Rewriting Logic and Its Applications - 12th International Workshop, 2018

Associative Unification and Symbolic Reasoning Modulo Associativity in Maude.
Proceedings of the Rewriting Logic and Its Applications - 12th International Workshop, 2018

Symbolic Reasoning Methods in Rewriting Logic and Maude.
Proceedings of the Logic, Language, Information, and Computation, 2018

Modular Verification of Sequential Composition for Private Channels in Maude-NPA.
Proceedings of the Security and Trust Management - 14th International Workshop, 2018

Formal Design of Cloud Computing Systems in Maude.
Proceedings of the Formal Methods: Foundations and Applications - 21st Brazilian Symposium, 2018

Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2018

ROLA: A New Distributed Transaction Protocol and Its Formal Analysis.
Proceedings of the Fundamental Approaches to Software Engineering, 2018

2017
Strict coherence of conditional rewriting modulo axioms.
Theor. Comput. Sci., 2017

Quantitative Analysis of Consistency in NoSQL Key-Value Stores.
LITES, 2017

Dependency pairs for proving termination properties of conditional term rewriting systems.
J. Log. Algebr. Meth. Program., 2017

A Constructor-Based Reachability Logic for Rewrite Theories.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2017

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2017

Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking.
Proceedings of the Formal Methods and Software Engineering, 2017

2016
Normal forms and normal theories in conditional rewriting.
J. Log. Algebr. Meth. Program., 2016

Modeling and analyzing mobile ad hoc networks in Real-Time Maude.
J. Log. Algebr. Meth. Program., 2016

Metalevel Algorithms for Variant Satisfiability.
Proceedings of the Rewriting Logic and Its Applications - 11th International Workshop, 2016

Towards Generic Monitors for Object-Oriented Real-Time Maude Specifications.
Proceedings of the Rewriting Logic and Its Applications - 11th International Workshop, 2016

Formal modeling and analysis of RAMP transaction systems.
Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016

Strand spaces with choice via a process algebra semantics.
Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, 2016

Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2016

Order-Sorted Rewriting and Congruence Closure.
Proceedings of the Foundations of Software Science and Computation Structures, 2016

Built-in Variant Generation and Unification, and Their Applications in Maude 2.7.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
Semantics, distributed implementation, and formal analysis of KLAIM models in Maude.
Sci. Comput. Program., 2015

Constrained narrowing for conditional equational theories modulo axioms.
Sci. Comput. Program., 2015

Model checking linear temporal logic of rewriting formulas under localized fairness.
Sci. Comput. Program., 2015

Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study.
Sci. Comput. Program., 2015

Executable rewriting logic semantics of Orc and formal analysis of Orc programs.
J. Log. Algebr. Meth. Program., 2015

Analysis of the PKCS#11 API Using the Maude-NPA Tool.
Proceedings of the Security Standardisation Research - Second International Conference, 2015

Quantitative Analysis of Consistency in NoSQL Key-Value Stores.
Proceedings of the Quantitative Evaluation of Systems, 12th International Conference, 2015

Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2015

Variant-Based Satisfiability in Initial Algebras.
Proceedings of the Formal Techniques for Safety-Critical Systems, 2015

Localized Operational Termination in General Logics.
Proceedings of the Software, 2015

Formal Analysis of Leader Election in MANETs Using Real-Time Maude.
Proceedings of the Software, 2015

Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories.
Proceedings of the Programming Languages with Applications to Biology and Security, 2015

2014
Formal patterns for multirate distributed real-time systems.
Sci. Comput. Program., 2014

State space reduction in the Maude-NRL Protocol Analyzer.
Inf. Comput., 2014

A modular order-sorted equational generalization algorithm.
Inf. Comput., 2014

Formal Specification of Button-Related Fault-Tolerance Micropatterns.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

Rewriting Modulo SMT and Open System Analysis.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

2D Dependency Pairs for Proving Operational Termination of CTRSs.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

Strong and Weak Operational Termination of Order-Sorted Rewrite Theories.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

A Framework for Mobile Ad hoc Networks in Real-Time Maude.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

Infinite-State Model Checking of LTLR Formulas Using Narrowing.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA.
Proceedings of the Security and Trust Management - 10th International Workshop, 2014

Analysis of the IBM CCA Security API Protocols in Maude-NPA.
Proceedings of the Security Standardisation Research - First International Conference, 2014

Predicate Abstraction of Rewrite Theories.
Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Theories of Homomorphic Encryption, Unification, and the Finite Variant Property.
Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, 2014

Proving Operational Termination of Declarative Programs in General Logics.
Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, 2014

Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2014

ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance.
Proceedings of the Logics in Artificial Intelligence - 14th European Conference, 2014

Formal Modeling and Analysis of Cassandra in Maude.
Proceedings of the Formal Methods and Software Engineering, 2014

A rewriting-based forwards semantics for Maude-NPA.
Proceedings of the 2014 Symposium and Bootcamp on the Science of Security, 2014

Definition, Semantics, and Analysis of Multirate Synchronous AADL.
Proceedings of the FM 2014: Formal Methods, 2014

Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool.
Proceedings of the Specification, Algebra, and Software, 2014

Models for Logics and Conditional Constraints in Automated Proofs of Termination.
Proceedings of the Artificial Intelligence and Symbolic Computation, 2014

2013
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing.
Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

Formal Analysis of Fault-tolerant Group Key Management Using ZooKeeper.
Proceedings of the 13th IEEE/ACM International Symposium on Cluster, 2013

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.
Proceedings of the Automated Deduction - CADE-24, 2013

2012
Rewriting semantics of production rule sets.
J. Log. Algebr. Program., 2012

On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories.
J. Log. Algebr. Program., 2012

Order-sorted Equational Unification Revisited.
Electr. Notes Theor. Comput. Sci., 2012

A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting.
Electr. Notes Theor. Comput. Sci., 2012

PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude
Proceedings of the Proceedings First International Workshop on Formal Techniques for Safety-Critical Systems, 2012

Design and Analysis of Cloud-Based Architectures with KLAIM and Maude.
Proceedings of the Rewriting Logic and Its Applications - 9th International Workshop, 2012

Order-Sorted Equality Enrichments Modulo Axioms.
Proceedings of the Rewriting Logic and Its Applications - 9th International Workshop, 2012

Model Checking LTLR Formulas under Localized Fairness.
Proceedings of the Rewriting Logic and Its Applications - 9th International Workshop, 2012

Statistical Model Checking for Composite Actor Systems.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2012

State Space c-Reductions of Concurrent Systems in Rewriting Logic.
Proceedings of the Formal Methods and Software Engineering, 2012

Stable Availability under Denial of Service Attacks through Formal Patterns.
Proceedings of the Fundamental Approaches to Software Engineering, 2012

Proceedings of the Fundamental Approaches to Software Engineering, 2012

IBOS: A Correct-By-Construction Modular Browser.
Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012

Formal Patterns for Multi-rate Distributed Real-Time Systems.
Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions.
Proceedings of the Computer Security - ESORICS 2012, 2012

2011
Maude.
Proceedings of the Encyclopedia of Parallel Computing, 2011

Automated Model Synchronization: A Case Study on UML with Maude.
ECEASST, 2011

Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Incremental checking of well-founded recursive specifications modulo axioms.
Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption.
Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Verification of microarchitectural refinements in rule-based systems.
Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2011

Synchronous AADL and Its Formal Analysis in Real-Time Maude.
Proceedings of the Formal Methods and Software Engineering, 2011

The Rewriting Logic Semantics Project: A Progress Report.
Proceedings of the Fundamentals of Computation Theory - 18th International Symposium, 2011

Taming Distributed System Complexity through Formal Patterns.
Proceedings of the Formal Aspects of Component Software - 8th International Symposium, 2011

State/Event-Based LTL Model Checking under Parametric Generalized Fairness.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Proving Safety Properties of Rewrite Theories.
Proceedings of the Algebra and Coalgebra in Computer Science, 2011

PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool.
Proceedings of the Algebra and Coalgebra in Computer Science, 2011

2010
Algebraic simulations.
J. Log. Algebr. Program., 2010

Using the PALS Architecture to Verify a Distributed Topology Control Protocol for Wireless Multi-Hop Networks in the Presence of Node Failures
Proceedings of the Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems, 2010

Distributed Real-Time Emulation of Formally-Defined Patterns for Safe Medical Device Control
Proceedings of the Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems, 2010

Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family
Proceedings of the Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems, 2010

Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis
Proceedings of the Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems, 2010

A Formal Pattern Architecture for Safe Medical Systems.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

Twenty Years of Rewriting Logic.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

Folding Variant Narrowing and Optimal Variant Termination.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

The Linear Temporal Logic of Rewriting Maude Model Checker.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

A Dependency Pair Framework for A OR C-Termination.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA.
Proceedings of the Security and Trust Management - 6th International Workshop, 2010

A formal executable semantics of Verilog.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Coverset Induction with Partiality and Subsorts: A Powerlist Case Study.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems.
Proceedings of the Formal Methods and Software Engineering, 2010

vlogsl: A Strategy Language for Simulation-Based Verification of Hardware.
Proceedings of the Hardware and Software: Verification and Testing, 2010

Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude.
Proceedings of the Formal Techniques for Distributed Systems, 2010

Sequential Protocol Composition in Maude-NPA.
Proceedings of the Computer Security, 2010

2009
A rewriting logic approach to operational semantics.
Inf. Comput., 2009

A Graphical User Interface for Maude-NPA.
Electr. Notes Theor. Comput. Sci., 2009

A Rewriting Semantics for Maude Strategies.
Electr. Notes Theor. Comput. Sci., 2009

Operational Termination of Membership Equational Programs: the Order-Sorted Way.
Electr. Notes Theor. Comput. Sci., 2009

Variant Narrowing and Equational Unification.
Electr. Notes Theor. Comput. Sci., 2009

Web Services and Interoperability for the Maude Termination Tool.
Electr. Notes Theor. Comput. Sci., 2009

Methods for Proving Termination of Rewriting-based Programming Languages by Transformation.
Electr. Notes Theor. Comput. Sci., 2009

Order-Sorted Generalization.
Electr. Notes Theor. Comput. Sci., 2009

Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol.
Electr. Notes Theor. Comput. Sci., 2009

Algebraic Semantics of OCL-Constrained Metamodel Specifications.
Proceedings of the Objects, Components, Models and Patterns, 47th International Conference, 2009

Unification and Narrowing in Maude 2.4.
Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

MOMENT2: EMF Model Transformations in Maude.
Proceedings of the XIV Jornadas de Ingeniería del Software y Bases de Datos (JISBD 2009), 2009

Termination Modulo Combinations of Equational Theories.
Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

Rewriting Logic Semantics and Verification of Model Transformations.
Proceedings of the Fundamental Approaches to Software Engineering, 2009

Model-Checking DoS Amplification for VoIP Session Initiation.
Proceedings of the Computer Security, 2009

Order-Sorted Parameterization and Induction.
Proceedings of the Semantics and Algebraic Specification, 2009

2008
Design of Complex Cyber Physical Systems with Formalized Architectural Patterns.
Proceedings of the Software-Intensive Systems and New Computing Paradigms, 2008

Proving operational termination of membership equational programs.
Higher-Order and Symbolic Computation, 2008

Termination of just/fair computations in term rewriting.
Inf. Comput., 2008

Algebraic Stuttering Simulations.
Electr. Notes Theor. Comput. Sci., 2008

Reduction Semantics and Formal Analysis of Orc Programs.
Electr. Notes Theor. Comput. Sci., 2008

What Is a Multi-modeling Language?
Proceedings of the Recent Trends in Algebraic Development Techniques, 2008

The Real-Time Maude Tool.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Effectively Checking the Finite Variant Property.
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Order-sorted dependency pairs.
Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2008

Directed-Logical Testing for Functional Verification of Microprocessors.
Proceedings of the 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008), 2008

A Modular Equational Generalization Algorithm.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2008

Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

An Algebraic Semantics for MOF.
Proceedings of the Fundamental Approaches to Software Engineering, 2008

State Space Reduction in the Maude-NRL Protocol Analyzer.
Proceedings of the Computer Security, 2008

MTT: The Maude Termination Tool (System Description).
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Ugo Montanari in a Nutshell.
Proceedings of the Concurrency, 2008

The Temporal Logic of Rewriting: A Gentle Introduction.
Proceedings of the Concurrency, 2008

Theorem Proving Modulo Based on Boolean Equational Procedures.
Proceedings of the Relations and Kleene Algebra in Computer Science, 2008

2007
The rewriting logic semantics project.
Theor. Comput. Sci., 2007

Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic.
Theor. Comput. Sci., 2007

Maude's module algebra.
Sci. Comput. Program., 2007

A Rewriting Decision Procedure for Dijkstra-Scholten's Syllogistic Logic with Complements.
Revista Colombiana de Computación, 2007

Semantics and pragmatics of Real-Time Maude.
Higher-Order and Symbolic Computation, 2007

Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols.
Higher-Order and Symbolic Computation, 2007

A Rewriting Logic Approach to Operational Semantics (Extended Abstract).
Electr. Notes Theor. Comput. Sci., 2007

Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics.
Electr. Notes Theor. Comput. Sci., 2007

Abstraction and Completeness for Real-Time Maude.
Electr. Notes Theor. Comput. Sci., 2007

Electr. Notes Theor. Comput. Sci., 2007

A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis.
Electr. Notes Theor. Comput. Sci., 2007

Partial Order Reduction for Rewriting Semantics of Programming Languages.
Electr. Notes Theor. Comput. Sci., 2007

Narrowing and Rewriting Logic: from Foundations to Applications.
Electr. Notes Theor. Comput. Sci., 2007

Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer.
Electr. Notes Theor. Comput. Sci., 2007

Deduction, Strategies, and Rewriting.
Electr. Notes Theor. Comput. Sci., 2007

A Systematic Approach to Uncover Security Flaws in GUI Logic.
Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), 2007

On the Completeness of Context-Sensitive Order-Sorted Specifications.
Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

Symbolic Model Checking of Infinite-State Systems Using Narrowing.
Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

Real-time rewriting semantics of orc.
Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

Mobile Maude.
Proceedings of the All About Maude, 2007

Specifying Parameterized Data Structures in Maude.
Proceedings of the All About Maude, 2007

Playing with Maude.
Proceedings of the All About Maude, 2007

Some Tools.
Proceedings of the All About Maude, 2007

Core Maude Grammar.
Proceedings of the All About Maude, 2007

Complete List of Maude Commands.
Proceedings of the All About Maude, 2007

Debugging and Troubleshooting.
Proceedings of the All About Maude, 2007

A Sampler of Application Areas.
Proceedings of the All About Maude, 2007

Object-Oriented Modules.
Proceedings of the All About Maude, 2007

Full Maude: Extending Core Maude.
Proceedings of the All About Maude, 2007

User Interfaces and Metalanguage Applications.
Proceedings of the All About Maude, 2007

Metaprogramming Applications.
Proceedings of the All About Maude, 2007

Reflection, Metalevel Computation, and Strategies.
Proceedings of the All About Maude, 2007

LTL Model Checking.
Proceedings of the All About Maude, 2007

Model Checking Invariants Through Search.
Proceedings of the All About Maude, 2007

Object-Based Programming.
Proceedings of the All About Maude, 2007

Predefined Data Modules.
Proceedings of the All About Maude, 2007

Module Operations.
Proceedings of the All About Maude, 2007

System Modules.
Proceedings of the All About Maude, 2007

A Hierarchy of Data Types: From Trees to Sets.
Proceedings of the All About Maude, 2007

Functional Modules.
Proceedings of the All About Maude, 2007

Syntax and Basic Parsing.
Proceedings of the All About Maude, 2007

Using Maude.
Proceedings of the All About Maude, 2007

Introduction.
Proceedings of the All About Maude, 2007

Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties.
Proceedings of the Foundations of Security Analysis and Design V, 2007

The Maude Formal Tool Environment.
Proceedings of the Algebra and Coalgebra in Computer Science, 2007

2006
A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties.
Theor. Comput. Sci., 2006

Semantic foundations for generalized rewrite theories.
Theor. Comput. Sci., 2006

Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude.
Formal Methods in System Design, 2006

The Rewriting Logic Semantics Project.
Electr. Notes Theor. Comput. Sci., 2006

PMaude: Rewrite-based Specification Language for Probabilistic Object Systems.
Electr. Notes Theor. Comput. Sci., 2006

Joseph Goguen (1941-2006).
Bulletin of the EATCS, 2006

Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 9th International Workshop, 2006

A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

From OBJ to Maude and Beyond.
Proceedings of the Algebra, Meaning, and Computation, 2006

State Space Reduction of Rewrite Theories Using Invisible Transitions.
Proceedings of the Algebraic Methodology and Software Technology, 2006

2005
A Verification Logic for Rewriting Logic.
J. Log. Comput., 2005

Operational termination of conditional term rewriting systems.
Inf. Process. Lett., 2005

Real-Time Maude 2.1.
Electr. Notes Theor. Comput. Sci., 2005

Symbolic Reachability Analysis Using Narrowing and its Application to Verification of Cryptographic Protocols.
Electr. Notes Theor. Comput. Sci., 2005

Towards a Strategy Language for Maude.
Electr. Notes Theor. Comput. Sci., 2005

Modular Rewriting Semantics in Practice.
Electr. Notes Theor. Comput. Sci., 2005

Computational Logical Frameworks and Generic Program Analysis Technologies.
Proceedings of the Verified Software: Theories, 2005

Localized Fairness: A Rewriting Semantics.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

A Sufficient Completeness Reasoning Tool for Partial Specifications.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Natural Narrowing for General Term Rewriting Systems.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Termination of Fair Computations in Term Rewriting.
Proceedings of the Logic for Programming, 2005

A Rewriting Logic Sampler.
Proceedings of the Theoretical Aspects of Computing, 2005

A rewriting-based inference system for the NRL protocol analyzer: grammar generation.
Proceedings of the 2005 ACM workshop on Formal methods in security engineering, 2005

Complete Symbolic Reachability Analysis Using Back-and-Forth Narrowing.
Proceedings of the Algebra and Coalgebra in Computer Science: First International Conference, 2005

A Categorical Approach to Simulations.
Proceedings of the Algebra and Coalgebra in Computer Science: First International Conference, 2005

Functorial Semantics of Rewrite Theories.
Proceedings of the Formal Methods in Software and Systems Modeling, 2005

2004
Reflective metalogical frameworks.
ACM Trans. Comput. Log., 2004

Theoroidal Maps as Algebraic Simulations.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2004

Proving termination of membership equational programs.
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Natural Rewriting for General Term Rewriting Systems.
Proceedings of the Logic Based Program Synthesis and Transformation, 2004

Specification and Analysis of Real-Time Systems Using Real-Time Maude.
Proceedings of the Fundamental Approaches to Software Engineering, 2004

Formal Analysis of Java Programs in JavaFAN.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework.
Proceedings of the From Object-Orientation to Formal Methods, 2004

Modular Rewriting Semantics of Programming Languages.
Proceedings of the Algebraic Methodology and Software Technology, 2004

Formal JVM Code Analysis in JavaFAN.
Proceedings of the Algebraic Methodology and Software Technology, 2004

2003
Structured theories and institutions.
Theor. Comput. Sci., 2003

The Maude LTL Model Checker and Its Implementation.
Proceedings of the Model Checking Software, 2003

The Maude 2.0 System.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Executable Computational Logics: Combining Formal Methods and Programming Language Based System Design.
Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

Algebraic Theories for Contextual Pre-nets.
Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

Generalized Rewrite Theories.
Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

A Rewriting Based Model for Probabilistic Distributed Object Systems.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2003

Certifying and Synthesizing Membership Equational Proofs.
Proceedings of the FME 2003: Formal Methods, 2003

Equational Abstractions.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002
Specification of real-time and hybrid systems in rewriting logic.
Theor. Comput. Sci., 2002

Preface.
Theor. Comput. Sci., 2002

Theor. Comput. Sci., 2002

Reflection in conditional rewriting logic.
Theor. Comput. Sci., 2002

Maude: specification and programming in rewriting logic.
Theor. Comput. Sci., 2002

Symmetric Monoidal and Cartesian Double Categories as a Semantic Framework for Tile Logic.
Mathematical Structures in Computer Science, 2002

Towards Behavioral Maude: Behavioral Membership Equational Logic.
Electr. Notes Theor. Comput. Sci., 2002

The Maude LTL Model Checker.
Electr. Notes Theor. Comput. Sci., 2002

Reflection in Membership Equational Logic, Many-Sorted Equational Logic, Horn Logic with Equality, and Rewriting Logic.
Electr. Notes Theor. Comput. Sci., 2002

Tiling Transactions in Rewriting Logic.
Electr. Notes Theor. Comput. Sci., 2002

Pathway Logic: Symbolic Analysis of Biological Signaling.
Proceedings of the 7th Pacific Symposium on Biocomputing, 2002

Mapping Modular SOS to Rewriting Logic.
Proceedings of the Logic Based Program Synthesis and Tranformation, 2002

A Total Approach to Partial Algebraic Specification.
Proceedings of the Automata, Languages and Programming, 29th International Colloquium, 2002

Semantic Models for Distributed Object Reflection.
Proceedings of the ECOOP 2002, 2002

Maude as a Wide-Spectrum Framework for Formal Modeling and Analysis of Active Networks.
Proceedings of the 2002 DARPA Active Networks Conference and Exposition (DANCE 2002), 2002

2001
Report on ETAPS 2000.
ACM SIGSOFT Software Engineering Notes, 2001

Functorial Models for Petri Nets.
Inf. Comput., 2001

Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework.
Electr. Notes Theor. Comput. Sci., 2001

The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability).
Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude.
Proceedings of the Fundamental Approaches to Software Engineering, 2001

Rewriting Logic as a Unifying Framework for Petri Nets.
Proceedings of the Unifying Petri Nets, Advances in Petri Nets, 2001

2000
Semantic interoperation of open systems.
ACM SIGSOFT Software Engineering Notes, 2000

Maude.
ACM SIGSOFT Software Engineering Notes, 2000

Real-Time Maude: A Tool for Simulating and Analyzing Real-Time and Hybrid Systems.
Electr. Notes Theor. Comput. Sci., 2000

Parameterized Theories and Views in Full Maude 2.0.
Electr. Notes Theor. Comput. Sci., 2000

Rewriting Semantics of Meta-Objects and Composable Distributed Services.
Electr. Notes Theor. Comput. Sci., 2000

Towards Maude 2.0.
Electr. Notes Theor. Comput. Sci., 2000

Rewriting Logic and Maude: Concepts and Applications.
Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

Principles of Mobile Maude.
Proceedings of the Agent Systems, 2000

Specification and Formal Analysis of a PLAN Algorithm in Maude.
Proceedings of the 2000 ICDCS Workshops, April 10, 2000, Taipei, Taiwan, ROC, 2000

Rewriting Logic as a Metalogical Framework.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

Composing and Controlling Search in Reasoning Theories Using Mappings.
Proceedings of the Frontiers of Combining Systems, 2000

Rewriting Logic and Maude: a Wide-Spectrum Semantic Framework for Object-Based Distributed Systems.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems IV, 2000

Using Maude.
Proceedings of the Fundamental Approaches to Software Engineering, 2000

Maude Action Tool: Using Reflection to Map Action Semantics to Rewriting Logic.
Proceedings of the Algebraic Methodology and Software Technology. 8th International Conference, 2000

1999
Structured Theories and Institutions.
Electr. Notes Theor. Comput. Sci., 1999

Functorial semantics for Petri nets under the individual token philosophy.
Electr. Notes Theor. Comput. Sci., 1999

Towards a Verification Logic for Rewriting Logic.
Proceedings of the Recent Trends in Algebraic Development Techniques, 1999

The Maude System.
Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

Maude as a Formal Meta-tool.
Proceedings of the FM'99 - Formal Methods, 1999

Executable Tile Specifications for Process Calculi.
Proceedings of the Fundamental Approaches to Software Engineering, 1999

A Partial Order Event Model for Concurrent Objects.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

1998
Mapping OMRS to rewriting logic.
Electr. Notes Theor. Comput. Sci., 1998

An extensible module algebra for Maude.
Electr. Notes Theor. Comput. Sci., 1998

Maude as a metalanguage.
Electr. Notes Theor. Comput. Sci., 1998

Metalevel computation in Maude.
Electr. Notes Theor. Comput. Sci., 1998

Internal strategies in a rewriting implementation of tile systems.
Electr. Notes Theor. Comput. Sci., 1998

A Logical Framework for Distributed Systems and Communication Protocols.
Proceedings of the Formal Description Techniques and Protocol Specification, 1998

On the Semantics of GAEA.
Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, 1998

A Comparison of Petri Net Semantics under the Collective Token Philosophy.
Proceedings of the Advances in Computing Science, 1998

1997
May I Borrow Your Logic? (Transporting Logical Structures Along Maps).
Theor. Comput. Sci., 1997

On the Semantics of Place/Transition Petri Nets.
Mathematical Structures in Computer Science, 1997

Mapping tile logic into rewriting logic.
Proceedings of the Recent Trends in Algebraic Development Techniques, 1997

Membership algebra as a logical framework for equational specification.
Proceedings of the Recent Trends in Algebraic Development Techniques, 1997

Specification and Proof in Membership Equational Logic.
Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Representation Theorems for Petri Nets.
Proceedings of the Foundations of Computer Science: Potential - Theory, 1997

1996
Process versus Unfolding Semantics for Place/Transition Petri Nets.
Theor. Comput. Sci., 1996

Inclusions and Subtypes II: Higher-Order Case.
J. Log. Comput., 1996

Inclusions and Subtypes I: First-Order Case.
J. Log. Comput., 1996

Software Component Search.
Journal of Systems Integration, 1996

Specifying real-time systems in rewriting logic.
Electr. Notes Theor. Comput. Sci., 1996

Preface.
Electr. Notes Theor. Comput. Sci., 1996

Rewriting logic as a logical and semantic framework.
Electr. Notes Theor. Comput. Sci., 1996

Reflection and strategies in rewriting logic.
Electr. Notes Theor. Comput. Sci., 1996

Principles of Maude.
Electr. Notes Theor. Comput. Sci., 1996

Why OOP Needs New Semantic Foundations.
ACM Comput. Surv., 1996

Axiomatizing the Algebra of Net Computations and Processes.
Acta Inf., 1996

Rewriting Logic as a Semantic Framework for Concurrency: a Progress Report.
Proceedings of the CONCUR '96, 1996

Distributed Simulation of Parallel Executions.
Proceedings of the Proceedings 29st Annual Simulation Symposium (SS '96), 1996

1994
Compiling Rewriting onto SIMD and MIMD/SIMD Maschines.
Proceedings of the PARLE '94: Parallel Architectures and Languages Europe, 1994

Specification, Transformation, and Programming of Concurrent Systems in Rewriting Logic.
Proceedings of the Specification of Parallel Algorithms, 1994

The Rewrite Rule Machine Node Architecture and Its Performance.
Proceedings of the Parallel Processing: CONPAR 94, 1994

From Abstract Data Types to Logical Frameworks.
Proceedings of the Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30, 1994

On the Model of Computation of Place/Transition Petri Nets.
Proceedings of the Application and Theory of Petri Nets 1994, 1994

1993
Order-Sorted Algebra Solves the Constructor-Selector, Multiple Representation, and Coercion Problems
Inf. Comput., March, 1993

A Logical Semantics for Object-Oriented Databases.
Proceedings of the 1993 ACM SIGMOD International Conference on Management of Data, 1993

Proceedings of the Mathematical Foundations of Computer Science 1993, 1993

Solving the Inheritance Anomaly in Concurrent Object-Oriented Programming.
Proceedings of the ECOOP'93, 1993

1992
Final Algebras, Cosemicomputable Algebras and Degrees of Unsolvability.
Theor. Comput. Sci., 1992

Conditioned Rewriting Logic as a United Model of Concurrency.
Theor. Comput. Sci., 1992

Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations.
Theor. Comput. Sci., 1992

On the Semantics of Petri Nets.
Proceedings of the CONCUR '92, 1992

Proceedings of the Algebraic and Logic Programming, 1992

1991
From Petri Nets to Linear Logic through Categories: A Survey.
Int. J. Found. Comput. Sci., 1991

Parallel Programmming in Maude.
Proceedings of the Research Directions in High-Level Parallel Programming Languages, 1991

1990
Petri Nets Are Monoids
Inf. Comput., October, 1990

A Logical Theory of Concurrent Objects.
Proceedings of the Conference on Object-Oriented Programming Systems, 1990

Conditional Rewriting Logic: Deduction, Models and Concurrency.
Proceedings of the Conditional and Typed Rewriting Systems, 1990

Compiling Concurrent Rewriting onto the Rewrite Rule Machine.
Proceedings of the Conditional and Typed Rewriting Systems, 1990

Rewriting as a Unified Model of Concurrency.
Proceedings of the CONCUR '90, 1990

1989
Order-Sorted Unification.
J. Symb. Comput., 1989

Relating Models of Polymorphism.
Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989

Axiomatizing Net Computations and Processes
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

From Petri Nets to Linear Logic.
Proceedings of the Category Theory and Computer Science, 1989

Temporal Structures.
Proceedings of the Category Theory and Computer Science, 1989

1988
Petri Nets Are Monoids: A New Algebraic Foundation for Net Theory
Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

Operational Semantics of OBJ-3 (Extended Abstract).
Proceedings of the Automata, Languages and Programming, 15th International Colloquium, 1988

Software for the Rewrite Rule Machine.
Proceedings of the International Conference on Fifth Generation Computer Systems, 1988

1987
Remarks on Remarks on Many-Sorted Equational Logic.
SIGPLAN Notices, 1987

On the Axiomatization of "If-Then-Else".
SIAM J. Comput., 1987

Models and Equality for Logical Programming.
Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987

Order-Sorted Algebra solves the Constructor-Selector, Multiple
Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

Parameterized Programming in OBJ2.
Proceedings of the Proceedings, 9th International Conference on Software Engineering, Monterey, California, USA, March 30, 1987

An Introduction to OBJ 3.
Proceedings of the Conditional Term Rewriting Systems, 1987

Final Algebras, Cosemicomputable Algebras, and Degrees of Unsolvability.
Proceedings of the Category Theory and Computer Science, 1987

Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics.
Proceedings of the Research Directions in Object-Oriented Programming, 1987

1986
Remarks on remarks on many-sorted algebras with possibly emtpay carrier sets.
Bulletin of the EATCS, 1986

Concurrent term rewriting as a model of computation.
Proceedings of the Graph Reduction, Proceedings of a Workshop, Santa Fé, New Mexico, USA, September 29, 1986

EQLOG: Equality, Types, and Generic Modules For Logic Programming.
Proceedings of the Logic Programming: Functions, Relations, and Equations, 1986

1985
Principles of OBJ2.
Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

Operational Semantics for Order-Sorted Algebra.
Proceedings of the Automata, 1985

1984
Equality, Types, Modules, and (Why not ?) Generics for Logic Programming.
J. Log. Program., 1984

Unwinding and Inference Control.
Proceedings of the 1984 IEEE Symposium on Security and Privacy, Oakland, California, USA, April 29, 1984

Equality, Types, Modules and Generics for Logic Programming.
Proceedings of the Second International Logic Programming Conference, 1984

1983
Correctness of Recursive Parallel Nondeterministic Flow Programs.
J. Comput. Syst. Sci., 1983

1982
Completeness of many-sorted equational logic.
SIGPLAN Notices, 1982

Security Policies and Security Models.
Proceedings of the 1982 IEEE Symposium on Security and Privacy, 1982

Finding Safe Paths in a Faulty Environment.
Proceedings of the ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, 1982

Universal Realization, Persistent Interconnection and Implementation of Abstract Modules.
Proceedings of the Automata, 1982

1981
A Birkhoff-Like Theorem for Algebraic Classes of Interpretations of Program Schemes.
Proceedings of the Formalization of Programming Concepts, 1981

1977
Correctness of Recursive Flow Diagram Programs.
Proceedings of the Mathematical Foundations of Computer Science 1977, 1977

On Order-Complete Universal Algebra and Enriched Functorial Semantics.
Proceedings of the Fundamentals of Computation Theory, 1977

1974
Automata in semimodule categories.
Proceedings of the Category Theory Applied to Computation and Control, 1974