Javier Esparza | ||

Professor Chair for Foundations of Software Reliability and Theoretical Computer Science Faculty of Computer Science Technische Universität München orcid.org/0000-0001-9862-4919 Another photo Yet another photo | ||||||||||||||||||||

Coordinates |
| |||||||||||||||||||

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

Current teaching |
Summer 2019IN0018 Model Checking 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 |
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 | |||||||||||||||||||

Other publications | Physics (just two old papers) Computer Science in Medicine (very 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 Peregrine: Verification of Population Protocols | |||||||||||||||||||

Current students | Stefan Jaax Philipp Meyer Chana Weil-Kennedy Christoph Welzel | |||||||||||||||||||

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, Salomon Sickert, Alin Stefanescu, Dejvuth Suwimonteerabuth | |||||||||||||||||||

Current post-docs | Michael Luttenberger Mikhail Raskin Marijana Lazic | |||||||||||||||||||

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

Some current projects |
Parameterized Verification and Synthesis, ERC Advanced Grant Negotiations: A Model for Tractable Concurrency , DFG project Computer Aided Verification of Automata (CAVA), DFG project | |||||||||||||||||||

Some past projects |
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, 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 |
Black Ninjas in the Dark: Formal Analysis of Population Protocols (LICS' 18) 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 Member of the Steering Committee of CONCUR, FOSSACS, ICALP, and GandALF RAIRO Theoretical Informatics and Applications IFIP Working Group 2.2 Formal Description of Programming Concepts | |||||||||||||||||||

Recent and upcomingevents |
VMCAI 2019 20th International Conference on
Verification, Model Checking, and Abstract Interpretation | |||||||||||||||||||

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