Javier Esparza Professor Chair for Foundations of Software Reliability and Theoretical Computer Science Department of Informatics, Technical University of Munich orcid.org/0000000198624919 Another (more recent, but not very recent) photo Yet another photo 

Coordinates 


About me  Short biography Curriculum vitae (PDF)  
Current teaching 
Winter 2020/2021 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 

Books (downloadable for free) 
A course on automata theory My book on freechoice Petri nets with Jörg Desel (can be downloaded here) My book on unfoldings, a partialorder modelchecking 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 OmegaAutomata Strix: LTL Synthesis 

Current students  A.R. Balasuramanian Philipp Czerner Martin Helfrich Philipp K. J. Meyer Chana WeilKennedy 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 PrensaNieto,
Christine Röckl,
Stefan Römer,
Maximilian Schlund,
Claus Schröter,
Stefan Schwoon,
Salomon Sickert,
Alin Stefanescu,
Dejvuth Suwimonteerabuth 

Current postdocs  Michael Luttenberger Mikhail Raskin Marijana Lazic  
Past postdocs  Michael Blondin, Tomas Brazdil, Christopher Broadbendt, Antoine DurandGasselin, 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 CyberPhysical 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 ContextAware Systems. Subproject of the Sonderforschungsbereich 627 Nexus An AutomataTheoretic Approach to Software Model Checking. EPSRC grant Automatic Synthesis of Distributed Systems. EPSRC grant ADVANCE, Advanced Validation Techniques for Telecommunication Protocols. ISTFET project 

Some invited talks and courses 
Course on Formal Analysis of Population Protocols (Marktoberdorf Summer School 2019) A Unified Translation of LTL into omegaAutomata (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 2010SPIN 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 BigOh 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 Infinitestate Systems (Marktoberdorf Summer School 2005) Verifying Probabilistic Procedural Programs (FSTTCS 2004) An AutomataTheoretic 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) Controlflow 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 