Contact
People
 |
 |
|
| 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 |
Summer 2013 IN0018 Vorlesung Diskrete Wahrscheinlichkeitstheorie IN2052 Vorlesung 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 linear and constraint programming to verification problems Semantics of parallel programming languages Analysis and synthesis of asynchronous circuits | |||||||||||||||||||
| Publications in computer science |
NEW! (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 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 | |||||||||||||||||||
| Current students | Andreas Gaiser
Christian Kern
Jan Kretinsky
Rene Neumann
Maximilian Schlund
| |||||||||||||||||||
| Past students | Stefan Kiefer,
Michael Luttenberger,
Richard Mayr,
Stephan Melzer, Leonor Prensa-Nieto, Stefan Römer, Christine Röckl, Claus Schröter, Stefan Schwoon, Alin Stefanescu, Dejvuth Suwimonteerabuth. | |||||||||||||||||||
| Current post-docs |
Michael Luttenberger | |||||||||||||||||||
| Past post-docs | Tomas Brazdil,
Keijo Heljanko,
Barbara König,
Jörg Kreiker (born Bauer),
Antonin Kucera, Monika Maidl, Dirk Nowotka, Stefan Schwoon | |||||||||||||||||||
| Current projects | Computer Aided Verification of Automata (CAVA), DFG project Polynomial systems on semirings: foundations, algorithms, applications, DFG project Program and Model Analysis (PUMA), DFG doctorate program | |||||||||||||||||||
| Some past projects | 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 | 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 RAIRO Theoretical Informatics and Applications IFIP Working Group 2.2 Formal Description of Programming Concepts | |||||||||||||||||||
| Recent and upcoming events |
CAV 2013 25th Conference on Computer Aided Verification LICS2013 Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, LATA 2013 7th International Conference on Language and Automata Theory and Applications WATA 2012 6th International Workshop Weighted Automata: Theory and Applications TACAS 2012 18th Conference on Tools and Algorithms for the Construction and Analysis of Systems Petri Nets 2012 33rd Conference on Application and Theory of Petri Nets and Concurrency ICALP 2012 The 39th International Colloquium on Automata, Languages and Programming | |||||||||||||||||||
 | Personal | Some movies I like
Some books I like
A speech |
|
