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 |
| |||||||||||||||||||

About me | Short biography Curriculum vitae (PDF) | |||||||||||||||||||

Current teaching |
Winter 2017/2018IN2041 Automata Theory and Formal Languages IN0015 Diskrete Strukturen | |||||||||||||||||||

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 at DBLP My papers at Google Scholar Database of the Chair (with search by year, type, or author) | |||||||||||||||||||

Other publications | Physics (just two papers) Computer Science in Medicine (old papers) | |||||||||||||||||||

Software | PEP: 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 students | Stefan Jaax Philipp Meyer Salomon Sickert | |||||||||||||||||||

Past students | Andreas Gaiser, Philipp Hoffmann, Christian Kern,
Stefan Kiefer,
Jan Kretinsky,
Michael Luttenberger, Richard Mayr, Stephan Melzer, Rene Neumann, Leonor Prensa-Nieto, Christine Röckl, Stefan Römer, Maximilian Schlund, Claus Schröter, Stefan Schwoon, Alin Stefanescu, Dejvuth Suwimonteerabuth | |||||||||||||||||||

Current post-docs | Michael Blondin Michael Luttenberger | |||||||||||||||||||

Past post-docs |
Tomas Brazdil,
Christopher Broadendt,
Antoine Durand-Gasselin,
Keijo Heljanko,
Loig Jezequel,
Barbara König,
Jörg Kreiker,
Antonin Kucera,
Monika Maidl,
Dirk Nowotka,
Stefan Schwoon,
Dejvuth Suwimonteerabuth | |||||||||||||||||||

Some current projects | Negotiations: A Model for Tractable Concurrency (CAVA), DFG project Computer 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 talksand 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 membershipsand professional activities | Logical Methods in Computer Science Acta Informatica RAIRO Theoretical Informatics and Applications IFIP Working Group 2.2 Formal Description of Programming Concepts | |||||||||||||||||||

Recent and upcomingevents |
LICS 2018
Thirty-Third Annual ACM/IEEE Symposium on
Logic in Computer Science TIME 2017 24th International Symposium on Temporal Representation and Reasoning FOSSACS 2017 20th International Conference on Foundations of Software Science and Computation Structures CAV 2017 29th International Conference on Computer-Aided Verifciation CONCUR 2017 28th International Conference on Concurrency Theory CSR 2017 12th International Computer Science Symposium in Russia | |||||||||||||||||||

Personal | Some movies I like
Some books I like
A speech |