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

Coordinates 


About me  Short biography Curriculum vitae (PDF)  
Current teaching 
Winter 2022/2023 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 Roland Guttenberg Martin Helfrich Chana WeilKennedy Christoph Welzel  
Past students 
Andreas Gaiser, Philipp Hoffmann,
Stefan Jaax,
Christian Kern,
Stefan Kiefer,
Jan Kretinsky,
Michael Luttenberger,
Richard Mayr,
Stephan Melzer,
Philipp K. 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 

Current postdocs  Michael Luttenberger 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, Mikhail Raskin, Fabian Reiter, Stefan Schwoon, Dejvuth Suwimonteerabuth  
Some current projects 
Parameterized Verification and Synthesis (PaVeS), ERC Advanced Grant Continuous Verification of CyberPhysical Systems, ConVeY DFG Research Training Group 

Some past projects 
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 CONCUR, FOSSACS, ICALP, 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 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 