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

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 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 Summer 2017
IN0011   Einführung in die Theoretische Informatik
IN2052   Petri Nets
(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
(Still unpublished) 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 online (detailed list including bibtex info)
My papers at DBLP
My papers at Google Scholar
Database of the Chair   (with search by year, type, or author)
Other publicationsPhysics (just two papers)   Computer Science in Medicine (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
Current studentsStefan Jaax     Philipp Hoffmann     Philipp Meyer     Rene Neumann     Salomon Sickert    
Past studentsAndreas Gaiser, Christian Kern, Stefan Kiefer, Jan Kretinsky, Michael Luttenberger, Richard Mayr,
Stephan Melzer, Leonor Prensa-Nieto, Christine Röckl, Stefan Römer, Maximilian Schlund, Claus Schröter, Stefan Schwoon, Alin Stefanescu, Dejvuth Suwimonteerabuth
Current post-docsMichael Blondin     Michael Luttenberger    
Past post-docs Tomas Brazdil, Christopher Broadendt, Antoine Durand-Gasselin, Keijo Heljanko, Loig Jezequel, Barbara König, Jörg Kreiker, Antonin Kucera, Monika Maidl, Dirk Nowotka, Stefan Schwoon, Dejvuth Suwimonteerabuth
Some current projectsComputer Aided Verification of Automata (CAVA), DFG project
Program and Model Analysis (PUMA), DFG doctorate program
Some past projects 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
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
RAIRO Theoretical Informatics and Applications
IFIP Working Group 2.2 Formal Description of Programming Concepts
Recent and upcoming
FOSSACS 2017 20th International Conference on Foundations of Software Science and Computation Structures
CAV 2017 29th International Conference on Computer-Aided Verifciation
CONCUR 2017 28th International Conference on Concurrency Theory
CSR 2017 12th International Computer Science Symposium in Russia
DISC 2016 30th International Symposium on Distributed Computing
ATVA 2016 14th International Symposium on Automated Technology for Verification and Analysis
PersonalSome movies I like     Some books I like     A speech