Javier Esparza

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

Another photo     Yet another one, older     ... and a really old 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: Department of Computer Science, Technical University of Munich, Boltzmannstr. 3, 85748 Garching, 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 Summer 2024
IN0011   Einführung in die Theoretische Informatik
IN2052   Petri Nets
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)
Automata Theory: An Algorithmic Approach with Michael Blondin
Free-choice Petri nets with Jörg Desel
Unfoldings. A Partial-Order Approach to Model Checking with Keijo Heljanko
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 Philipp Czerner     Roland Guttenberg     Valentin Krasotin     ,
Past students A.R. Balasuramanian, Andreas Gaiser, Philipp Hoffmann, Stefan Jaax, Martin Helfrich, Christian Kern, Stefan Kiefer, Jan Kretinsky, Michael Luttenberger, Richard Mayr, Stephan Melzer, Klara 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, Christoph Welzel
Current post-docs
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 Continuous Verification of Cyber-Physical Systems, ConVeY DFG Research Training Group
Some past projects Parameterized Verification and Synthesis (PaVeS), ERC Advanced Grant
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 FOSSACS and GandALF
IFIP Working Group 2.2 Formal Description of Programming Concepts
IFIP Working Group 1.8 Concurrency Theory
Some recent and
upcoming events
TACAS 2024  29th Conference on Tools and Algorithms for the Construction and Analysis of Systems
LICS 2024
Marktoberdorf Summer School 2023
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