I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Javier Esparza

Chair for Foundations of Software Reliability and Theoretical Computer Science
Faculty of Computer Science
Technische Universität München
ORCID iD iconorcid.org/0000-0001-9862-4919

Another photo
Yet another photo

 Office: 03.11.054 (third floor, block 11), Mathematics and Computer Science Building    
How to find it
 E-mail: esparza AT in DOT tum DOT de
 Snail: Institut für Informatik, Technische Universität München,
Boltzmannstr. 3, 85748 Garching bei München, Germany.
 Phone: +49 (89) 289 17204
 Fax: +49 (89) 289 17207
 Assistant:   Claudia Link, +49 (89) 289 17234
About me Short biography     Curriculum vitae (PDF)    
Current teaching Winter 2020/2021
IN2041   Automata Theory and Formal Languages
(no order)
Algorithms and tools for the design and verification of reactive and distributed systems
Verification of systems with infinitely many states
Software Model Checking
Program analysis
Formal models for distributed systems: Petri nets and process algebras
Logic and automata theory
Analysis of probabilistic systems
Applications of constraint solvers to verification problems
Semantics of parallel programming languages
Analysis and synthesis of asynchronous circuits
Publications in
computer science
Lecture notes on automata theory
My book on free-choice Petri nets with Jörg Desel (can be downloaded here)
My book on unfoldings, a partial-order model-checking technique, with Keijo Heljanko (can be downloaded here)
My papers at DBLP
My papers at Google Scholar
Other publicationsPhysics (just two old papers)   Computer Science in Medicine (very old papers)
SoftwarePEP: Programming Environment Based on Petri Nets
The Model-Checking Kit: An Integrated Platform of Model Checking Tools
Moped: A Model Checker for Pushdown Systems
jMoped: A Test Environment for Java Programs
Rabinizer: Small Deterministic Rabin Automata from LTL Formulas
Peregrine: Verification of Population Protocols
Current students A.R. Balasuramanian     Martin Helfrich     Philipp Meyer     Chana Weil-Kennedy     Christoph Welzel    
Past studentsAndreas Gaiser, Philipp Hoffmann, Stefan Jaax, Christian Kern, Stefan Kiefer, Jan Kretinsky, Michael Luttenberger, Richard Mayr, Stephan Melzer, Rene Neumann, Leonor Prensa-Nieto, Christine Röckl, Stefan Römer, Maximilian Schlund, Claus Schröter, Stefan Schwoon, Salomon Sickert, Alin Stefanescu, Dejvuth Suwimonteerabuth
Current post-docsMichael Luttenberger     Mikhail Raskin     Marijana Lazic
Past post-docs Michael Blondin, Tomas Brazdil, Christopher Broadbendt, Antoine Durand-Gasselin, Keijo Heljanko, Loig Jezequel, Barbara König, Jörg Kreiker, Antonin Kucera, Monika Maidl, Dirk Nowotka, Fabian Reiter, Stefan Schwoon, Dejvuth Suwimonteerabuth
Some current projects Parameterized Verification and Synthesis, ERC Advanced Grant
Computer Aided Verification of Automata (CAVA), DFG project
Some past projects Negotiations: A Model for Tractable Concurrency , DFG project
Program and Model Analysis (PUMA), DFG doctorate program
Polynomial systems on semirings: foundations, algorithms, applications, DFG project
Algorithms for Software Model Checking, DFG project
Formal methods for Modelling and Analysing Mobile Context-Aware Systems, a subproject of the Sonderforschungsbereich 627 Nexus
An Automata-Theoretic Approach to Software Model Checking, EPSRC grant
Automatic Synthesis of Distributed Systems, EPSRC grant
ADVANCE Advanced Validation Techniques for Telecommunication Protocols, IST-FET project
Some invited talks
and courses
Course on Formal Analysis of Population Protocols (Marktoberdorf Summer School '19)
A Unified Translation of LTL into omega-Automata (Jerusalem, Paris '18)
Black Ninjas in the Dark: Formal Analysis of Population Protocols (LICS' 18)
Verification of Population Protocols (PV' 15)
Parameterized Verification (Marktoberdorf Summer School '15)
Deterministic Negotiations: Concurrency for Free (CONCUR '14)
Solving fixed point equations over semirings (CIAA '14)
Keeping a Crowd Safe: On the Complexity of Parametrized Verification (STACS '14)
A Brief History of Strahler Numbers (LATA '14)
A Perfect Model for Finite Verification (AVM '12)
A False History of True Concurrency: From Petri to Tools (ICGT '10-SPIN '10)
Stochastic Process Creation (MFCS '09, VMCAI '10)
Solving Monotone Polynomial Equations (TCS '08)
Newtonian Program Analysis (ICALP '08, ETAPS '10)
SDSIrep: A Reputation System based on SDSI (several places)
Beyond Big-Oh Analysis in Automata Theory (GAMES '07)
Computation of certificate chains with alternating pushdown systems (ATVA '06)
Rewriting models of boolean programs (RTA '06)
Computing rewards in probabilistic pushdown systems (PAuL '06)
Verification of Infinite-state Systems (Marktoberdorf Summer School '05)
Verifying Probabilistic Procedural Programs (FSTTCS '04)
An Automata-Theoretic Approach to Software Model Checking (POPL '04)
Logic in Automatic Verification (LMPS '03)
A False History of True Concurrency (LMPS '03)
Some Applications of Petri Nets to the Analysis of Parameterised Systems (WISP '03)
Control-flow in Software Model Checking (AVIS '03)
Model checking infinite state systems (SMC-02, Bertinoro)
Model checking finite and infinite state systems (Second School on Computational Logic)
Verifying broadcast protocols (VCL '00)
Verification with unfoldings (CONCUR '99)
Grammars as processes (ETAPS '99)
Some memberships
and professional
Logical Methods in Computer Science
Acta Informatica
Member of the Steering Committee of CONCUR, FOSSACS, ICALP, and GandALF
RAIRO Theoretical Informatics and Applications
IFIP Working Group 2.2 Formal Description of Programming Concepts
Recent and upcoming
Petri Nets 2020   41st International Conference on Application and Theory of Petri Nets and Concurrency
FORTE 2020   40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems
ATVA 2019   International Symposium on Automated Technology for Verification and Analysis
Petri Nets 2019   40th International Conference on Application and Theory of Petri Nets and Concurrency
VMCAI 2019   20th International Conference on Verification, Model Checking, and Abstract Interpretation
PersonalSome movies I like     Some books I like     A speech