| 2025 | FASE | Capturing System Designs with Formal Executable Specifications. | Jos Meseguer |
| 2025 | LOPSTR | Symbolic Computation and Verification Methods in Maude. | Jos Meseguer |
| 2025 | PPDP | Formalizing Languages with Binding Operators in Rewriting Logic. | Maribel Fernndez, Jos Meseguer |
| 2024 | PPDP | NuITP: An Inductive Theorem Prover for Equational Program Verification. | Francisco J. Durn, Santiago Escobar, Jos Meseguer, Julia Sapia |
| 2024 | PPDP | Programming Open Distributed Systems in Maude. | Francisco Durn, Steven Eker, Santiago Escobar, Narciso Mart-Oliet, Jos Meseguer, Rubn Rubio, Carolyn L. Talcott |
| 2023 | ESORICS | Protocol Dialects as Formal Patterns. | D. Galn, Vctor Garca, Santiago Escobar, Catherine A. Meadows, Jos Meseguer |
| 2022 | CADE | Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description). | Francisco Durn, Steven Eker, Santiago Escobar, Narciso Mart-Oliet, Jos Meseguer, Rubn Rubio, Carolyn L. Talcott |
| 2020 | INDOCRYPT | Protocol Analysis with Time. | Damin Aparicio-Snchez, Santiago Escobar, Catherine Meadows, Jos Meseguer, Julia Sapia |
| 2020 | LOPSTR | Symbolic Computation in Maude: Some Tapas. | Jos Meseguer |
| 2019 | JELIA | ACUOS | Mara Alpuente, Demis Ballis, Angel Cuenca-Ortega, Santiago Escobar, Jos Meseguer |
| 2019 | TACAS | Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. | Si Liu, Peter Csaba lveczky, Min Zhang, Qi Wang, Jos Meseguer |
| 2018 | FASE | ROLA: A New Distributed Transaction Protocol and Its Formal Analysis. | Si Liu, Peter Csaba lveczky, Keshav Santhanam, Qi Wang, Indranil Gupta, Jos Meseguer |
| 2018 | LOPSTR | Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. | Mara Alpuente, Angel Cuenca-Ortega, Santiago Escobar, Jos Meseguer |
| 2018 | LPAR | Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA. | Antonio Gonzlez-Burgueo, Damin Aparicio-Snchez, Santiago Escobar, Catherine Meadows, Jos Meseguer |
| 2018 | WoLLIC | Symbolic Reasoning Methods in Rewriting Logic and Maude. | Jos Meseguer |
| 2017 | ICFEM | Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking. | Si Liu, Peter Csaba lveczky, Jatin Ganhotra, Indranil Gupta, Jos Meseguer |
| 2017 | LOPSTR | Variant-Based Decidable Satisfiability in Initial Algebras with Predicates. | Ral Gutirrez, Jos Meseguer |
| 2017 | LOPSTR | A Constructor-Based Reachability Logic for Rewrite Theories. | Stephen Skeirik, Andrei Stefanescu, Jos Meseguer |
| 2016 | CADE | Built-in Variant Generation and Unification, and Their Applications in Maude 2.7. | Francisco Durn, Steven Eker, Santiago Escobar, Narciso Mart-Oliet, Jos Meseguer, Carolyn L. Talcott |
| 2016 | FOSSACS | Order-Sorted Rewriting and Congruence Closure. | Jos Meseguer |
| 2016 | LOPSTR | Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms. | Mara Alpuente, Angel Cuenca-Ortega, Santiago Escobar, Jos Meseguer |
| 2016 | PPDP | Strand spaces with choice via a process algebra semantics. | Fan Yang, Santiago Escobar, Catherine Meadows, Jos Meseguer, Sonia Santiago |
| 2016 | SAC | Formal modeling and analysis of RAMP transaction systems. | Si Liu, Peter Csaba lveczky, Muntasir Raihan Rahman, Jatin Ganhotra, Indranil Gupta, Jos Meseguer |
| 2015 | LOPSTR | Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras. | Jos Meseguer, Stephen Skeirik |
| 2014 | AISC | Models for Logics and Conditional Constraints in Automated Proofs of Termination. | Salvador Lucas, Jos Meseguer |
| 2014 | FM | Definition, Semantics, and Analysis of Multirate Synchronous AADL. | Kyungmin Bae, Peter Csaba lveczky, Jos Meseguer |
| 2014 | ICFEM | Formal Modeling and Analysis of Cassandra in Maude. | Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta, Jos Meseguer |
| 2014 | JELIA | ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance. | Mara Alpuente, Santiago Escobar, Javier Espert, Jos Meseguer |
| 2014 | LOPSTR | Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems. | Salvador Lucas, Jos Meseguer, Ral Gutirrez |
| 2014 | PPDP | Proving Operational Termination of Declarative Programs in General Logics. | Salvador Lucas, Jos Meseguer |
| 2014 | PPDP | Theories of Homomorphic Encryption, Unification, and the Finite Variant Property. | Fan Yang, Santiago Escobar, Catherine Meadows, Jos Meseguer, Paliath Narendran |
| 2013 | CADE | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. | Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2013 | CCGRID | Formal Analysis of Fault-tolerant Group Key Management Using ZooKeeper. | Stephen Skeirik, Rakesh B. Bobba, Jos Meseguer |
| 2012 | ESORICS | Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. | Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2012 | FASE | The SynchAADL2Maude Tool. | Kyungmin Bae, Peter Csaba lveczky, Jos Meseguer, Abdullah Al-Nayeem |
| 2012 | FASE | Stable Availability under Denial of Service Attacks through Formal Patterns. | Jonas Eckhardt, Tobias Mhlbauer, Musab AlTurki, Jos Meseguer, Martin Wirsing |
| 2012 | ICFEM | State Space c-Reductions of Concurrent Systems in Rewriting Logic. | Alberto Lluch-Lafuente, Jos Meseguer, Andrea Vandin |
| 2011 | CALCO | PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. | Musab AlTurki, Jos Meseguer |
| 2011 | CALCO | Proving Safety Properties of Rewrite Theories. | Camilo Rocha, Jos Meseguer |
| 2011 | CAV | State/Event-Based LTL Model Checking under Parametric Generalized Fairness. | Kyungmin Bae, Jos Meseguer |
| 2011 | FCT | The Rewriting Logic Semantics Project: A Progress Report. | Jos Meseguer, Grigore Rosu |
| 2011 | ICFEM | Synchronous AADL and Its Formal Analysis in Real-Time Maude. | Kyungmin Bae, Peter Csaba lveczky, Abdullah Al-Nayeem, Jos Meseguer |
| 2011 | MEMOCODE | Verification of microarchitectural refinements in rule-based systems. | Nirav Dave, Michael Katelman, Myron King, Arvind, Jos Meseguer |
| 2011 | PPDP | Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. | Santiago Escobar, Deepak Kapur, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Ralf Sasse |
| 2011 | PPDP | Incremental checking of well-founded recursive specifications modulo axioms. | Felix Schernhammer, Jos Meseguer |
| 2010 | ESORICS | Sequential Protocol Composition in Maude-NPA. | Santiago Escobar, Catherine Meadows, Jos Meseguer, Sonia Santiago |
| 2010 | FORTE | Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. | Peter Csaba lveczky, Artur Boronat, Jos Meseguer |
| 2010 | ICFEM | Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems. | Jos Meseguer, Peter Csaba lveczky |
| 2010 | ITP | Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. | Joe Hendrix, Deepak Kapur, Jos Meseguer |
| 2010 | LPAR | Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories. | Camilo Rocha, Jos Meseguer |
| 2010 | MEMOCODE | A formal executable semantics of Verilog. | Patrick O'Neil Meredith, Michael Katelman, Jos Meseguer, Grigore Rosu |
| 2009 | ESORICS | Model-Checking DoS Amplification for VoIP Session Initiation. | Ravinder Shankesi, Musab AlTurki, Ralf Sasse, Carl A. Gunter, Jos Meseguer |
| 2009 | FASE | Rewriting Logic Semantics and Verification of Model Transformations. | Artur Boronat, Reiko Heckel, Jos Meseguer |
| 2008 | CADE | MTT: The Maude Termination Tool (System Description). | Francisco Durn, Salvador Lucas, Jos Meseguer |
| 2008 | ESORICS | State Space Reduction in the Maude-NRL Protocol Analyzer. | Santiago Escobar, Catherine Meadows, Jos Meseguer |
| 2008 | FASE | An Algebraic Semantics for MOF. | Artur Boronat, Jos Meseguer |
| 2008 | LOPSTR | A Modular Equational Generalization Algorithm. | Mara Alpuente, Santiago Escobar, Jos Meseguer, Pedro Ojeda |
| 2008 | MEMOCODE | Directed-Logical Testing for Functional Verification of Microprocessors. | Michael Katelman, Jos Meseguer, Santiago Escobar |
| 2008 | PPDP | Order-sorted dependency pairs. | Salvador Lucas, Jos Meseguer |
| 2008 | TACAS | The Real-Time Maude Tool. | Peter Csaba lveczky, Jos Meseguer |
| 2007 | CALCO | The Maude Formal Tool Environment. | Manuel Clavel, Francisco Durn, Joe Hendrix, Salvador Lucas, Jos Meseguer, Peter Csaba lveczky |
| 2007 | PPDP | Real-time rewriting semantics of orc. | Musab AlTurki, Jos Meseguer |
| 2007 | SP | A Systematic Approach to Uncover Security Flaws in GUI Logic. | Jos Meseguer, Ralf Sasse, Helen J. Wang, Yi-Min Wang |
| 2006 | CADE | A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. | Joe Hendrix, Jos Meseguer, Hitoshi Ohsaki |
| 2005 | CALCO | A Categorical Approach to Simulations. | Miguel Palomino, Jos Meseguer, Narciso Mart-Oliet |
| 2005 | CALCO | Complete Symbolic Reachability Analysis Using Back-and-Forth Narrowing. | Prasanna Thati, Jos Meseguer |
| 2005 | CCS | A rewriting-based inference system for the NRL protocol analyzer: grammar generation. | Santiago Escobar, Catherine Meadows, Jos Meseguer |
| 2005 | ICTAC | A Rewriting Logic Sampler. | Jos Meseguer |
| 2005 | LPAR | Termination of Fair Computations in Term Rewriting. | Salvador Lucas, Jos Meseguer |
| 2004 | CADE | Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. | Jos Meseguer, Grigore Rosu |
| 2004 | CAV | Formal Analysis of Java Programs in JavaFAN. | Azadeh Farzan, Feng Chen, Jos Meseguer, Grigore Rosu |
| 2004 | FASE | Specification and Analysis of Real-Time Systems Using Real-Time Maude. | Peter Csaba lveczky, Jos Meseguer |
| 2004 | LOPSTR | Natural Rewriting for General Term Rewriting Systems. | Santiago Escobar, Jos Meseguer, Prasanna Thati |
| 2004 | PEPM | Proving termination of membership equational programs. | Francisco Durn, Salvador Lucas, Jos Meseguer, Claude March, Xavier Urbain |
| 2003 | CADE | Equational Abstractions. | Jos Meseguer, Miguel Palomino, Narciso Mart-Oliet |
| 2003 | FM | Certifying and Synthesizing Membership Equational Proofs. | Grigore Rosu, Steven Eker, Patrick Lincoln, Jos Meseguer |
| 2003 | ICALP | Generalized Rewrite Theories. | Roberto Bruni, Jos Meseguer |
| 2003 | MEMOCODE | Executable Computational Logics: Combining Formal Methods and Programming Language Based System Design. | Jos Meseguer |
| 2002 | ECOOP | Semantic Models for Distributed Object Reflection. | Jos Meseguer, Carolyn L. Talcott |
| 2002 | ICALP | A Total Approach to Partial Algebraic Specification. | Jos Meseguer, Grigore Rosu |
| 2002 | LOPSTR | Mapping Modular SOS to Rewriting Logic. | Christiano de Oliveira Braga, Edward Hermann Haeusler, Jos Meseguer, Peter D. Mosses |
| 2002 | PSB | Pathway Logic: Symbolic Analysis of Biological Signaling. | Steven Eker, Merrill Knapp, Keith Laderoute, Patrick Lincoln, Jos Meseguer, M. Kemal Snmez |
| 2001 | FASE | Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude. | Peter Csaba lveczky, Mark Keaton, Jos Meseguer, Carolyn L. Talcott, Steve Zabele |
| 2000 | FASE | Using Maude. | Manuel Clavel, Francisco Durn, Steven Eker, Patrick Lincoln, Narciso Mart-Oliet, Jos Meseguer, Jose F. Quesada |
| 1999 | CONCUR | A Partial Order Event Model for Concurrent Objects. | Jos Meseguer, Carolyn L. Talcott |
| 1999 | FASE | Executable Tile Specifications for Process Calculi. | Roberto Bruni, Jos Meseguer, Ugo Montanari |
| 1999 | FM | Maude as a Formal Meta-tool. | Manuel Clavel, Francisco Durn, Steven Eker, Jos Meseguer, Mark-Oliver Stehr |
| 1998 | FLOPS | On the Semantics of GAEA. | Hiroshi Ishikawa, Takuo Watanabe, Kokichi Futatsugi, Jos Meseguer, Hideyuki Nakashima |
| 1998 | FORTE | A Logical Framework for Distributed Systems and Communication Protocols. | Jos Meseguer |
| 1996 | CONCUR | Rewriting Logic as a Semantic Framework for Concurrency: a Progress Report. | Jos Meseguer |
| 1994 | COMPASS | From Abstract Data Types to Logical Frameworks. | Jos Meseguer, Narciso Mart-Oliet |
| 1993 | ECOOP | Solving the Inheritance Anomaly in Concurrent Object-Oriented Programming. | Jos Meseguer |
| 1993 | MFCS | May I Borrow Your Logic? | Maura Cerioli, Jos Meseguer |
| 1993 | SIGMOD | A Logical Semantics for Object-Oriented Databases. | Jos Meseguer, Xiaolei Qian |
| 1992 | CONCUR | On the Semantics of Petri Nets. | Jos Meseguer, Ugo Montanari, Vladimiro Sassone |
| 1990 | CONCUR | Rewriting as a Unified Model of Concurrency. | Jos Meseguer |
| 1990 | OOPSLA | A Logical Theory of Concurrent Objects. | Jos Meseguer |
| 1989 | LICS | Axiomatizing Net Computations and Processes | Pierpaolo Degano, Jos Meseguer, Ugo Montanari |
| 1989 | POPL | Relating Models of Polymorphism. | Jos Meseguer |
| 1988 | ICALP | Operational Semantics of OBJ-3 (Extended Abstract). | Claude Kirchner, Hlne Kirchner, Jos Meseguer |
| 1988 | LICS | Petri Nets Are Monoids: A New Algebraic Foundation for Net Theory | Jos Meseguer, Ugo Montanari |
| 1987 | ICSE | Parameterized Programming in OBJ2. | Kokichi Futatsugi, Joseph A. Goguen, Jos Meseguer, Koji Okada |
| 1987 | LICS | Order-Sorted Algebra solves the Constructor-Selector, Multiple | Joseph A. Goguen, Jos Meseguer |
| 1985 | ICALP | Operational Semantics for Order-Sorted Algebra. | Joseph A. Goguen, Jean-Pierre Jouannaud, Jos Meseguer |
| 1985 | POPL | Principles of OBJ2. | Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, Jos Meseguer |
| 1984 | ICLP | Equality, Types, Modules and Generics for Logic Programming. | Joseph A. Goguen, Jos Meseguer |
| 1984 | SP | Unwinding and Inference Control. | Joseph A. Goguen, Jos Meseguer |
| 1982 | ICALP | Universal Realization, Persistent Interconnection and Implementation of Abstract Modules. | Joseph A. Goguen, Jos Meseguer |
| 1982 | PODC | Finding Safe Paths in a Faulty Environment. | Danny Dolev, Jos Meseguer, Marshall C. Pease |
| 1982 | SP | Security Policies and Security Models. | Joseph A. Goguen, Jos Meseguer |
| 1977 | FCT | On Order-Complete Universal Algebra and Enriched Functorial Semantics. | Jos Meseguer |
| 1977 | MFCS | Correctness of Recursive Flow Diagram Programs. | Joseph A. Goguen, Jos Meseguer |