About

Jose Meseguer is a professor at the Siebel School of Computing and Data Science at the University of Illinois Urbana-Champaign. He holds an education in Mathematics from the University of Zaragoza, obtained in 1975 with honors. His research areas include Programming Languages, Formal Methods, and Software Engineering. He has taught courses such as Program Verification, Concurrent Programming Languages, and Topics in Automated Deduction. His recent contributions have been recognized by the ACM for his work in the computing field. His professional contact information includes a phone number and email, and he is based at the Thomas M. Siebel Center for Computer Science.

Research topics

• Computer Science
• Programming language
• Artificial Intelligence
• Discrete mathematics
• Engineering
• Distributed computing
• Pure mathematics
• Mathematics
• Systems engineering
• Theoretical computer science

Selected publications

• Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification

  Journal of Logical and Algebraic Methods in Programming · 2025-01-18 · 4 citations

  article1st authorCorresponding
  PublisherDOI

• DM-Check: Verifying invariants of concurrent systems by deductive model checking

  Journal of Logical and Algebraic Methods in Programming · 2025-12-02

  articleOpen access

  [EN] We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is combined with inductive theorem proving to discharge inductive verification conditions that ensure useful symbolic state space reductions. An obvious combination is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible combination. In this paper we focus instead on a new deductive model checking methodology to verify invariants -including inductive invariants- of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle. Inductive verification conditions not discharged automatically by the oracle are dealt with by commands that refine some constrained patterns by useful semantic equivalences, and by using an inductive theorem prover in interactive mode. This methodology is demonstrated by means of concurrent system examples using two Maude tools working in tandem: the DM-Check narrowing-based symbolic model checker, and the NuITP inductive theorem prover.

  PublisherDOI

• Capturing System Designs with Formal Executable Specifications

  Lecture notes in computer science · 2025-01-01 · 2 citations

  book-chapterOpen access1st authorCorresponding

  Abstract Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trustworthiness can be developed in a faster and much more efficient way by capturing system designs with formal executable specifications and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of formal patterns . The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications is also discussed an illustrated with examples.

  PublisherOA PDFDOI

• Programming and Verifying Actor Systems in Rewriting Logic

  Lecture notes in computer science · 2025-09-24

  book-chapter1st authorCorresponding
  PublisherDOI

• Symbolic Computation and Verification Methods in Maude

  Lecture notes in computer science · 2025-09-09

  book-chapter1st authorCorresponding
  PublisherDOI

• Protocol Dialects as Formal Patterns

  Lecture notes in computer science · 2024-01-01 · 2 citations

  book-chapterOpen accessSenior author
  PublisherOA PDFDOI

• Programming Open Distributed Systems in Maude

  2024-09-04 · 4 citations

  articleOpen access

  Maude is a high-performance logical framework based on rewriting logic and supporting formal specification, verification and declarative programming of concurrent systems. Since most concurrent open systems are made up of actor-like objects that communicate with each other through message passing, Maude provides special features to support their specification, verification and programming. Since open systems are heterogeneous, involving widely different kinds of objects such as sensors, actuators, devices, databases, graphical user interfaces, and so on, Maude supports declarative message-passing interaction between Maude objects and a wide variety of heterogeneous external objects. In this paper we explain and illustrate a methodology where an open system can first be designed and verified in Maude and then implemented as a distributed system of heterogeneous objects in a way that seamlessly bridges the gap between its formal specification and verification and its distributed implementation.

  PublisherDOI

• Verifying Invariants by Deductive Model Checking

  Lecture notes in computer science · 2024-01-01 · 4 citations

  book-chapter
  PublisherDOI

• Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification

  arXiv (Cornell University) · 2024-05-03 · 1 citations

  preprintOpen access1st authorCorresponding

  An inductive inference system for proving validity of formulas in the initial algebra $T_{\mathcal{E}}$ of an order-sorted equational theory $\mathcal{E}$ is presented. It has 20 inference rules, but only 9 of them require user interaction; the remaining 11 can be automated as simplification rules. In this way, a substantial fraction of the proof effort can be automated. The inference rules are based on advanced equational reasoning techniques, including: equationally defined equality predicates, narrowing, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting, ordered rewriting, and recursive path orderings. All these techniques work modulo axioms $B$, for $B$ any combination of associativity and/or commutativity and/or identity axioms. Most of these inference rules have already been implemented in Maude's NuITP inductive theorem prover.

  PublisherOA PDFDOI

• Equivalence, and Property Internalization and Preservation for Equational Programs

  Lecture notes in computer science · 2024-01-01 · 2 citations

  book-chapter1st authorCorresponding
  PublisherDOI

Recent grants

• TC: Medium: Collaborative Research: Rewriting Logic Foundations for Verification and Programming of Next-Generation Trustworthy Web-Based Systems

  NSF · $300k · 2009–2013

• TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude

  NSF · $250k · 2013–2016

Frequent coauthors

• Joseph A. Goguen

  110 shared

• Narciso Martı́-Oliet

  83 shared

• Santiago Escobar

  Universitat Politècnica de València

  77 shared

• Francisco Durán

  Universidad de Málaga

  71 shared

• Steven Eker

  SRI International

  71 shared

• Jean-Yves L’Excellent

  66 shared

• David Padua

  64 shared

• Iain Duff

  Centre Européen de Recherche et de Formation Avancée en Calcul Scientifique

  64 shared

Labs

• Siebel School of Computing and Data SciencePI

Education

• Ph.D., Mathematics

  University of Zaragoza

  1975

Awards & honors

• ACM Recognizes Meseguer, Tong for Contributions to the Compu…