I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Javier Esparza

Professor
Chair for Foundations of Software Reliability and Theoretical Computer Science
Faculty of Computer Science
Technische Universität München

Another photo
Yet another photo



 
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: Institut 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 2016
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 constraint solvers to verification problems
Semantics of parallel programming languages
Analysis and synthesis of asynchronous circuits
 
Publications in
computer science
(Still unpublished) Lecture notes 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)
My papers online (detailed list including bibtex info)
My papers at DBLP
My papers at Google Scholar
Database of the Chair   (with search by year, type, or author)
Other publicationsPhysics (just two papers)   Computer Science in Medicine (old papers)
 
SoftwarePEP: Programming Environment Based on Petri Nets
The Model-Checking Kit: An Integrated Platform of Model Checking Tools
Moped: A Model Checker for Pushdown Systems
jMoped: A Test Environment for Java Programs
Rabinizer: Small Deterministic Rabin Automata from LTL Formulas
Current studentsStefan Jaax     Philipp Hoffmann     Philipp Meyer     Rene Neumann    
 
Past studentsAndreas Gaiser, Christian Kern, Stefan Kiefer, Jan Kretinsky, Michael Luttenberger, Richard Mayr,
Stephan Melzer, Leonor Prensa-Nieto, Christine Röckl, Stefan Römer, Maximilian Schlund,
Claus Schröter, Stefan Schwoon, Alin Stefanescu, Dejvuth Suwimonteerabuth
 
Current post-docsChristopher Broadbent     Michael Luttenberger     Dejvuth Suwimonteerabuth
Past post-docs Tomas Brazdil, Antoine Durand-Gasselin, Keijo Heljanko, Loig Jezequel, Barbara König, Jörg Kreiker, Antonin Kucera, Monika Maidl, Dirk Nowotka, Stefan Schwoon
Some current projectsComputer Aided Verification of Automata (CAVA), DFG project
Program and Model Analysis (PUMA), DFG doctorate program
 
Some past projects 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, a 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
Verification of Population Protocols (PV' 15)
Parameterized Verification (Marktoberdorf Summer School '15)
Deterministic Negotiations: Concurrency for Free (CONCUR '14)
Solving fixed point equations over semirings (CIAA '14)
Keeping a Crowd Safe: On the Complexity of Parametrized Verification (STACS '14)
A Brief History of Strahler Numbers (LATA '14)
A Perfect Model for Finite Verification (AVM '12)
A False History of True Concurrency: From Petri to Tools (ICGT '10-SPIN '10)
Stochastic Process Creation (MFCS '09, VMCAI '10)
Solving Monotone Polynomial Equations (TCS '08)
Newtonian Program Analysis (ICALP '08, ETAPS '10)
SDSIrep: A Reputation System based on SDSI (several places)
Beyond Big-Oh Analysis in Automata Theory (GAMES '07)
Computation of certificate chains with alternating pushdown systems (ATVA '06)
Rewriting models of boolean programs (RTA '06)
Computing rewards in probabilistic pushdown systems (PAuL '06)
Verification of Infinite-state Systems (Marktoberdorf Summer School '05)
Verifying Probabilistic Procedural Programs (FSTTCS '04)
An Automata-Theoretic Approach to Software Model Checking (POPL '04)
Logic in Automatic Verification (LMPS '03)
A False History of True Concurrency (LMPS '03)
Some Applications of Petri Nets to the Analysis of Parameterised Systems (WISP '03)
Control-flow in Software Model Checking (AVIS '03)
Model checking infinite state systems (SMC-02, Bertinoro)
Model checking finite and infinite state systems (Second School on Computational Logic)
Verifying broadcast protocols (VCL '00)
Verification with unfoldings (CONCUR '99)
Grammars as processes (ETAPS '99)
Some memberships
and professional
activities
Logical Methods in Computer Science
Acta Informatica
International Journal on Foundations of Computer Science
RAIRO Theoretical Informatics and Applications
IFIP Working Group 2.2 Formal Description of Programming Concepts
 
Recent and upcoming
events
DISC 2016 30th International Symposium on Distributed Computing
ATVA 2016 14th International Symposium on Automated Technology for Verification and Analysis
SAS 2016 23rd International Static Analysis Symposium
CAV 2016  28th Conference on Computer Aided Verification
TACAS 2016  22nd Conference on Tools and Algorithms for the Construction and Analysis of Systems
LPAR 20  20th Conference on Logic for Programming, Artificial Intelligence and Reasoning
LATA 2016  10th International Conference on Language and Automata Theory and Applications
VMCAI 2016  International Conference on Verification, Model Checking, and Abstract Interpretation
FSTTCS 2015  IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
GandALF 2015  Sixth Internatioal Symposium on Games, Automata, Logics and Formal Verification
RP 2015  9th International Workshop on Reachability Problems
PersonalSome movies I like     Some books I like     A speech