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 one, more recent     ... and a recent one

 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: Fakultät für Informatik, Technische Universität München, Boltzmannstr. 3, 85748 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 2022/2023
IN2041   Automata Theory and Formal Languages
Interests (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 linear and constraint programming to verification problems
Semantics of parallel programming languages
Analysis and synthesis of asynchronous circuits
(downloadable for free)
A course 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)
Papers in
computer science
Google Scholar
Other publications Physics (just two papers)   Computer Science in Medicine (old papers)
Some software
developed at my group
Rabinizer: Small Deterministic Rabin Automata from LTL Formulas
Peregrine: Verification of Population Protocols
Owl: Tools for Omega-Automata
Strix: LTL Synthesis
Current students A.R. Balasuramanian     Philipp Czerner     Roland Guttenberg     Martin Helfrich     Christoph Welzel    
Past students Andreas Gaiser, Philipp Hoffmann, Stefan Jaax, Christian Kern, Stefan Kiefer, Jan Kretinsky, Michael Luttenberger, Richard Mayr, Stephan Melzer, Philipp K. J. Meyer, Rene Neumann, Leonor Prensa-Nieto, Christine Röckl, Stefan Römer, Maximilian Schlund, Claus Schröter, Stefan Schwoon, Salomon Sickert, Alin Stefanescu, Dejvuth Suwimonteerabuth, Chana Weil-Kennedy
Current post-docs Michael Luttenberger     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, Mikhail Raskin, Fabian Reiter, Stefan Schwoon, Dejvuth Suwimonteerabuth
Some current projects Parameterized Verification and Synthesis (PaVeS), ERC Advanced Grant
Continuous Verification of Cyber-Physical Systems, ConVeY DFG Research Training Group
Some past projects Computer Aided Verification of Automata (CAVA). DFG project
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. 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
State Complexity of Population Protocols (FSTTCS 2021)
How I Give a Talk (Video) (Logic Mentoring Workshop 2021)
Back to the Future: A Fresh Look at Linear Temporal Logic (Richard M. Karp Distinguished Lecture, Berkeley) (Video)
Course on Formal Analysis of Population Protocols (Marktoberdorf Summer School 2019)
A Unified Translation of LTL into omega-Automata (Jerusalem, Paris, 2018)
Black Ninjas in the Dark: Formal Analysis of Population Protocols (LICS 2018)
Verification of Population Protocols (PV 2015)
Parameterized Verification (Marktoberdorf Summer School 2015)
Deterministic Negotiations: Concurrency for Free (CONCUR 2014)
Solving fixed point equations over semirings (CIAA 2014)
Keeping a Crowd Safe: On the Complexity of Parametrized Verification (STACS 2014)
A Brief History of Strahler Numbers (LATA 2014)
A Perfect Model for Finite Verification (AVM 2012)
A False History of True Concurrency: From Petri to Tools (ICGT 2010-SPIN 2010)
Stochastic Process Creation (MFCS 2009, VMCAI 2010)
Solving Monotone Polynomial Equations (TCS 2008)
Newtonian Program Analysis (ICALP 2008, ETAPS 2010)
SDSIrep: A Reputation System based on SDSI (several places)
Beyond Big-Oh Analysis in Automata Theory (GAMES 2007)
Computation of certificate chains with alternating pushdown systems (ATVA 2006)
Rewriting models of boolean programs (RTA 2006)
Computing rewards in probabilistic pushdown systems (PAuL 2006)
Verification of Infinite-state Systems (Marktoberdorf Summer School 2005)
Verifying Probabilistic Procedural Programs (FSTTCS 2004)
An Automata-Theoretic Approach to Software Model Checking (POPL 2004)
Logic in Automatic Verification (LMPS 2003)
A False History of True Concurrency (LMPS 2003)
Some Applications of Petri Nets to the Analysis of Parameterised Systems (WISP \'03)
Control-flow in Software Model Checking (AVIS 2003)
Model checking infinite state systems (SMC 2002, Bertinoro)
Model checking finite and infinite state systems (Second School on Computational Logic 2001)
Verifying broadcast protocols (VCL 2000)
Verification with unfoldings (CONCUR 1999)
Grammars as processes (ETAPS 1999)
Some memberships
and professional
Logical Methods in Computer Science
Member of the Steering Committee of CONCUR, FOSSACS, ICALP, and GandALF
IFIP Working Group 2.2 Formal Description of Programming Concepts
IFIP Working Group 1.8 Concurrency Theory
Some recent and
upcoming events
Marktoberdorf Summer School 2023 Participate!
CAV 2023 35th International Conference on Computer Aided Verification
TACAS 2023  29th Conference on Tools and Algorithms for the Construction and Analysis of Systems
GandALF 2022  Thirteenth International Symposium on Games, Automata, Logics, and Formal Verification
TACAS 2022  28th Conference on Tools and Algorithms for the Construction and Analysis of Systems
VMCAI 2022  23rd International Conference on Verification, Model Checking, and Abstract Interpretation
Personal Some movies I like     Some books I like     A speech