José Meseguer

Orcid: 0000-0003-4779-3848

Affiliations:
  • University of Illinois Urbana-Champaign, Thomas Siebel Center for Computer Science, Urbana-Champaign, IL, USA
  • SRI International, Menlo Park, CA, USA (former)
  • Stanford University, Centre for the Study of Language and Information, CA, USA (former)
  • University of Santiago de Compostela, Faculty of Science, Spain (former)
  • University of Zaragoza, Faculty of Science, Spain (PhD 1975)


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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification.
CoRR, 2024

Equivalence, and Property Internalization and Preservation for Equational Programs.
Proceedings of the Rewriting Logic and Its Applications - 15th International Workshop, 2024

Verifying Invariants by Deductive Model Checking.
Proceedings of the Rewriting Logic and Its Applications - 15th International Workshop, 2024

Programming Open Distributed Systems in Maude.
Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, 2024

NuITP: An Inductive Theorem Prover for Equational Program Verification.
Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, 2024

2023
Variants and satisfiability in the infinitary unification wonderland.
J. Log. Algebraic Methods Program., August, 2023

The Maude strategy language.
J. Log. Algebraic Methods Program., August, 2023

Protocol Dialects as Formal Patterns.
Proceedings of the Computer Security - ESORICS 2023, 2023

Optimizing Maude Programs via Program Specialization.
Proceedings of the Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems, 2023

2022
Bridging the semantic gap between qualitative and quantitative models of distributed systems.
Proc. ACM Program. Lang., 2022

Order-sorted equational generalization algorithm revisited.
Ann. Math. Artif. Intell., 2022

On Ground Convergence and Completeness of Conditional Equational Program Hierarchies.
Proceedings of the Rewriting Logic and Its Applications - 14th International Workshop, 2022

Checking Sufficient Completeness by Inductive Theorem Proving.
Proceedings of the Rewriting Logic and Its Applications - 14th International Workshop, 2022

An Efficient Canonical Narrowing Implementation for Protocol Analysis.
Proceedings of the Rewriting Logic and Its Applications - 14th International Workshop, 2022

Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description).
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Building Correct-by-Construction Systems with Formal Patterns.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2022

2021
Protocol Analysis with Time and Space.
Proceedings of the Protocols, Strands, and Logic, 2021

2020
Generalized rewrite theories, coherence completion, and symbolic methods.
J. Log. Algebraic Methods Program., 2020

Ground confluence of order-sorted conditional specifications modulo axioms.
J. Log. Algebraic Methods Program., 2020

Programming and symbolic computation in Maude.
J. Log. Algebraic Methods Program., 2020

A partial evaluation framework for order-sorted equational programs modulo axioms.
J. Log. Algebraic Methods Program., 2020

The 2D Dependency Pair Framework for Conditional Rewrite Systems - Part II: Advanced Processors and Implementation Techniques.
J. Autom. Reason., 2020

A Constructor-Based Reachability Logic for Rewrite Theories.
Fundam. Informaticae, 2020

Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms.
Fundam. Informaticae, 2020

Verification of the IBOS Browser Security Properties in Reachability Logic.
Proceedings of the Rewriting Logic and Its Applications - 13th International Workshop, 2020

Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification.
Proceedings of the Rewriting Logic and Its Applications - 13th International Workshop, 2020

Variant Satisfiability of Parameterized Strings.
Proceedings of the Rewriting Logic and Its Applications - 13th International Workshop, 2020

Variants in the Infinitary Unification Wonderland.
Proceedings of the Rewriting Logic and Its Applications - 13th International Workshop, 2020

Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs.
Proceedings of the NASA Formal Methods - 12th International Symposium, 2020

Symbolic Computation in Maude: Some Tapas.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2020

Protocol Analysis with Time.
Proceedings of the Progress in Cryptology - INDOCRYPT 2020, 2020

2019
Read atomic transactions with prevention of lost updates: ROLA and its formal analysis.
Formal Aspects Comput., 2019

Strand Spaces with Choice via a Process Algebra Semantics.
CoRR, 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

ACUOS<sup>2</sup>: 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
Variant-based satisfiability in initial algebras.
Sci. Comput. Program., 2018

Metalevel algorithms for variant satisfiability.
J. Log. Algebraic Methods Program., 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.
Leibniz Trans. Embed. Syst., 2017

Rewriting modulo SMT and open system analysis.
J. Log. Algebraic Methods Program., 2017

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

Equational formulas and pattern operations in initial order-sorted algebras.
Formal Aspects Comput., 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. Algebraic Methods Program., 2016

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

Effective Sequential Protocol Composition in Maude-NPA.
CoRR, 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
Order-sorted equality enrichments modulo axioms.
Sci. Comput. Program., 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. Algebraic Methods Program., 2015

Analysis of the PKCS#11 API Using the Maude-NPA Tool.
Proceedings of the Security Standardisation Research - Second International Conference, 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
Taming distributed system complexity through formal patterns.
Sci. Comput. Program., 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

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

Extensible Symbolic System Analysis.
Proceedings of the 28th International Workshop on Unification, 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
The rewriting logic semantics project: A progress report.
Inf. Comput., 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
Formalization and correctness of the PALS architectural pattern for distributed real-time systems.
Theor. Comput. Sci., 2012

Twenty years of rewriting logic.
J. Log. Algebraic Methods Program., 2012

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

Folding variant narrowing and optimal variant termination.
J. Log. Algebraic Methods Program., 2012

On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories.
J. Log. Algebraic Methods Program., 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

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

The SynchAADL2Maude Tool.
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.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.
Proceedings of the 25th International Workshop on Unification, 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

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. Algebraic Methods Program., 2010

An algebraic semantics for MOF.
Formal Aspects Comput., 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

Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits.
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 <i>A</i> OR <i>C</i>-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

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.
Proceedings of the Ninth Spanish Conference on Programming and Languages, 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

Equational abstractions.
Theor. Comput. Sci., 2008

Proving operational termination of membership equational programs.
High. Order Symb. Comput., 2008

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

A Rewriting Semantics for Maude Strategies.
Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, 2008

Operational Termination of Membership Equational Programs: the Order-Sorted Way.
Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, 2008

Order-sorted Equational Unification Revisited.
Proceedings of the Ninth International Workshop on Rule-Based Programming, 2008

Variant Narrowing and Equational Unification.
Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, 2008

Web Services and Interoperability for the Maude Termination Tool.
Proceedings of the Eighth Spanish Conference on Programming and Computer Languages, 2008

Methods for Proving Termination of Rewriting-based Programming Languages by Transformation.
Proceedings of the Eighth Spanish Conference on Programming and Computer Languages, 2008

A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting.
Proceedings of the Ninth International Workshop on Rule-Based Programming, 2008

Order-Sorted Generalization.
Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming, 2008

Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol.
Proceedings of the Third International Workshop on Security and Rewriting Techniques, 2008

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

Equational Unification by Variant Narrowing (Extended Abstract).
Proceedings of the 22nd International Workshop on Unification, 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

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.
Rev. Colomb. de Computación, 2007

Semantics and pragmatics of Real-Time Maude.
High. Order Symb. Comput., 2007

Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols.
High. Order Symb. Comput., 2007

A Rewriting Logic Approach to Operational Semantics (Extended Abstract).
Proceedings of the Fourth Workshop on Structural Operational Semantics, 2007

Algebraic Stuttering Simulations.
Proceedings of the Seventh Spanish Conference on Programming and Computer Languages, 2007

Reduction Semantics and Formal Analysis of Orc Programs.
Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, 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


Specifying Parameterized Data Structures in Maude.
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


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



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


Syntax and Basic Parsing.
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
Complete symbolic reachability analysis using back-and-forth narrowing.
Theor. Comput. Sci., 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 Syst. Des., 2006

Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics.
Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, 2006

Abstraction and Completeness for Real-Time Maude.
Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, 2006

Recent Advances in Real-Time Maude.
Proceedings of the 7th International Workshop on Rule Based Programming, 2006

A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis.
Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, 2006

Partial Order Reduction for Rewriting Semantics of Programming Languages.
Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, 2006

Narrowing and Rewriting Logic: from Foundations to Applications.
Proceedings of the 15th Workshop on Functional and (Constraint) Logic Programming, 2006

Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer.
Proceedings of the First International Workshop on Security and Rewriting Techniques, 2006

Deduction, Strategies, and Rewriting.
Proceedings of the 6th International Workshop on Strategies in Automated Deduction, 2006

Joseph Goguen (1941-2006).
Bull. 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

PMaude: Rewrite-based Specification Language for Probabilistic Object Systems.
Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, 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

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

Real-Time Maude 2.1.
Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, 2004

Towards a Strategy Language for Maude.
Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, 2004

Modular Rewriting Semantics in Practice.
Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, 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
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

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

Preface.
Theor. Comput. Sci., 2002

Rewriting logic: roadmap and bibliography.
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.
Math. Struct. Comput. Sci., 2002

Towards Behavioral Maude: Behavioral Membership Equational Logic.
Proceedings of the Coalgebraic Methods in Computer Science, 2002

The Maude LTL Model Checker.
Proceedings of the Fourth International Workshop on Rewriting logic and Its Applications, 2002

Tiling Transactions in Rewriting Logic.
Proceedings of the Fourth International Workshop on Rewriting logic and Its Applications, 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 Softw. Eng. Notes, 2001

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

Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework.
Proceedings of the Uniform Approaches to Graphical Process Specification Techniques, 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
Specification and proof in membership equational logic.
Theor. Comput. Sci., 2000

Semantic interoperation of open systems.
ACM SIGSOFT Softw. Eng. Notes, 2000

Maude.
ACM SIGSOFT Softw. Eng. Notes, 2000

Real-Time Maude: A Tool for Simulating and Analyzing Real-Time and Hybrid Systems.
Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 2000

Parameterized Theories and Views in Full Maude 2.0.
Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 2000

Rewriting Semantics of Meta-Objects and Composable Distributed Services.
Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 2000

Towards Maude 2.0.
Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 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.
Proceedings of the Conference on Category Theory and Computer Science, 1999

Functorial semantics for Petri nets under the individual token philosophy.
Proceedings of the Conference on Category Theory and Computer Science, 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.
Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

An extensible module algebra for Maude.
Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

Maude as a metalanguage.
Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

Metalevel computation in Maude.
Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

Internal strategies in a rewriting implementation of tile systems.
Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 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.
Math. Struct. Comput. Sci., 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

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.
J. Syst. Integr., 1996

Specifying real-time systems in rewriting logic.
Proceedings of the First International Workshop on Rewriting Logic and its Applications, 1996

Preface.
Proceedings of the First International Workshop on Rewriting Logic and its Applications, 1996

Rewriting logic as a logical and semantic framework.
Proceedings of the First International Workshop on Rewriting Logic and its Applications, 1996

Reflection and strategies in rewriting logic.
Proceedings of the First International Workshop on Rewriting Logic and its Applications, 1996

Principles of Maude.
Proceedings of the First International Workshop on Rewriting Logic and its Applications, 1996

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

Axiomatizing the Algebra of Net Computations and Processes.
Acta Informatica, 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

May I Borrow Your Logic?
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

Multiparadigm Logic Programming.
Proceedings of the Algebraic and Logic Programming, 1992

1991
From Petri Nets to Linear Logic.
Math. Struct. Comput. Sci., 1991

Temporal Structures.
Math. Struct. Comput. Sci., 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

Rewriting as a unified model of concurrency.
Proceedings of the Workshop on Object-based Concurrent Programming, 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

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

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.
ACM 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

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

1986
Foundations and extensions of object-oriented programming (abstract only).
Proceedings of the 1986 SIGPLAN Workshop on Object-Oriented Programming, 1986

Extensions and foundations of object-oriented programming.
Proceedings of the 1986 SIGPLAN Workshop on Object-Oriented Programming, 1986

Remarks on remarks on many-sorted algebras with possibly emtpay carrier sets.
Bull. 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.
ACM SIGPLAN Notices, 1982

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

Rapid prototyping: in the OBJ executable specification language.
Proceedings of the workshop on Rapid Prototyping, 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


  Loading...