Javier Esparza Professor Chair for Foundations of Software Reliability and Theoretical Computer Science Department of Computer Science Technische Universität München orcid.org/0000000198624919 Another photo Yet another one, older ... and a really old one. 

Coordinates 


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 

Books (downloadable for free) 
Automata Theory: An Algorithmic Approach with Michael Blondin Freechoice Petri nets with Jörg Desel Unfoldings. A PartialOrder Approach to Model Checking with Keijo Heljanko  
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  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 PrensaNieto,
Christine Röckl,
Stefan Römer,
Maximilian Schlund,
Claus Schröter,
Stefan Schwoon,
Salomon Sickert,
Alin Stefanescu,
Dejvuth Suwimonteerabuth,
Chana WeilKennedy,
Christoph Welzel 

Current postdocs  
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, Mikhail Raskin, Fabian Reiter, Stefan Schwoon, Dejvuth Suwimonteerabuth  
Some current projects 
Continuous Verification of CyberPhysical 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 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 
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 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 
TheoretiCS 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 