i
Javier Esparza

Professor
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



Coordinates
 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 Summer 2021
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
Books
(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
DBLP
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     Martin Helfrich     Philipp K. J. Meyer     Chana Weil-Kennedy     Christoph Welzel    
Past students Andreas 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-docs Michael 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 (PaVeS), ERC Advanced Grant
Computer Aided Verification of Automata (CAVA), DFG project
Continuous Verification of Cyber-Physical Systems, ConVeY DFG Research Training Group
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. 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
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
activities
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
Some recent and
upcoming events
MFCS 2020   45th International Symposium on Mathematical Foundations of Computer Science
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
Personal Some movies I like     Some books I like     A speech