Professor
Chair for Foundations of Software Reliability and Theoretical Computer Science
Department of Computer Science
Technische Universität München
orcid.org/0000-0001-9862-4919Another photo Yet another one, older ... and a really old one.
| 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: | Department of Computer Science, Technical University of Munich, Boltzmannstr. 3, 85748 Garching, Germany. |
| Phone: | +49 (89) 289 17204 |
| Fax: | +49 (89) 289 17207 |
| Assistant: | Claudia Link, +49 (89) 289 17234 |
IN0011 Einführung in die Theoretische Informatik
IN2052 Petri Nets
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
(downloadable for free)
Free-choice Petri nets with Jörg Desel
Unfoldings. A Partial-Order Approach to Model Checking with Keijo Heljanko
computer science
Google Scholar
developed at my group
Peregrine: Verification of Population Protocols
Owl: Tools for Omega-Automata
Strix: LTL Synthesis
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 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
and courses
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 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)
and professional
activities
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
upcoming events
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