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 2011 IN2049 Logic (in English) IN2007 Complexity Theory (in English), together with Dr. Jörg Kreiker | |||||||||||||||||||
| 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 |
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 | Polynomial systems on semiirngs: foundations, algorithms, applications, DFG project Computer-supported verification of automata constructions for model checking, 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 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 Theoretical Computer Science RAIRO Theoretical Informatics and Applications IFIP Working Group 2.2 Formal Description of Programming Concepts | |||||||||||||||||||
| Recent and upcoming events |
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 APLAS 2011 The Ninth Asian Symposium on programming Languages and Systems FSTTCS 2011 IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science GandALF 2011 Second International Symposium on Games, Automata, Logics and Formal Verification TASE 2011 5th IEEE and IFIP International Symposium on Theoretical Aspects of Software Engineering CALCO 2011 4th Conference on Algebra and Coalgebra Petri Nets 2011 32nd Conference on Application and Theory of Petri Nets and Concurrency TACAS 2011 17th Conference on Tools and Algorithms for the Construction and Analysis of Systems CONCUR 2011 22nd Conference on Concurrency Theory LPAR 17 17th Conference on Logic for Programming, Artificial Intelligence and Reasoning | |||||||||||||||||||
 | Personal | Some movies I like
Some books I like
A speech |
|
