Coordinates
building, room
052-00-005
+49 761 203 6953 (phone)
+49 761 203 8242 (fax)
Current state
Open for the research market. Here is my CV.Research interests
- Software verification and program analysis:
- Concurrency: modularity, compositionality, model-checking of multithreaded programs
- Specification: thread abstractions
- Abstract interpretation: smooth refinement and completeness.
- Privacy and security:
- Specification languages, formal models, logic, policies and preferences, privacy-enabled dynamic networks
- Access control, delegation, authorization.
- Combinatorics: enumeration.
- Future research:
- Polynomial verification of large program classes
- Emptiness of language intersection: complexity and algorithms
- Thread simulations, liveness, procedure abstractions under concurrency
- A working verifier for multithreaded C
- Verifying multithreaded programs with rich structure and semantics:
- heap
- probabilism
- recursion
- for multicore systems
- Modeling biological and social systems.
Teaching
- Offering student projects for Master, Bachelor, Diplom, team-project, etc. Both theory and practice tracks available.
- Offering seminar topics.
- Supervising Bachelor and PhD students (Jan Leike, Marco Muniz), Uni Freiburg, WS 2009-10.
- Verification lecture, Uni Freiburg, WS 2007-08.
- Seminar: Abstract Interpretation, Uni Freiburg, WS 2007-08.
- Seminar: Advanced topics in Model Checking, Uni Freiburg, SS 2007.
- Seminar: Software Model Checking, Uni Freiburg, WS 2006-07.
- Seminar: Software Model Checking, MPII, SS 2005.
- Reading Group at MPII, WS 2005 - SS 2006.
Publications
- PhD thesis, reviewed and defended.
- Abstract Threads, VMCAI 2010, Madrid, Springer. Its long version contains all the proofs. Conference participation partially funded by SIGPLAN PAC.
- Precise Thread-Modular Verification, SAS 2007, Kongens Lyngby, Springer. A long version is available: Thread-Modular Verification with Arbitrary Precision.
- Thread-Modular Verification is Cartesian Abstract Interpretation, ICTAC 2006, Tunis, Springer. Its long version Thread-Modular Verification and Cartesian Abstraction was presented at the TV 2006 workshop in Seattle.
- Polyominoes, polyedges and the digit game, Diploma thesis, Saarbrücken, 2004.
Talks
| Jan 2010, | VMCAI'10, Madrid, | Abstract Threads |
| Dec 2009, | UPMARC, Uppsala, | Owicki-Gries, Thread-Modular-Reasoning, Cartesian Abstraction |
| Oct 2009, | ARM, Cambridge, | Verification of Multithreaded Programs |
| Oct 2009, | Cambridge University, | Owicki-Gries, Thread-Modular-Reasoning, Cartesian Abstraction |
| Oct 2009, | Cambridge University, | Abstract Threads |
| Jun 2009, | MSR Cambridge, | SecPAL4Privacy |
| Feb 2009, | EPFL, Lausanne, | Counterexample–Guided Thread-Modular Verification |
| Sep 2008, | Freiburg University, | Cartesian Abstraction Refinement |
| Aug 2008, | ICMS, Edinburgh, | Cartesian Abstraction Refinement |
| Jul 2008, | MSR Redmond, | Concurrent Histories |
| May 2008, | MSR Redmond, | Cartesian Abstraction Refinement |
| Aug 2007, | SAS 07, Denmark, | Precise Thread-Modular Verification |
| Mar 2007, | EPFL, Lausanne, | Precise Thread-Modular Verification |
| Nov 2006, | ICTAC 2006, Tunis, | Thread-Modular Verification is Cartesian Abstract Interpretation. |
Tools
- AMTV: Automated Modular Thread Verifier. Checks safety of multithreaded programs. Licence: GPLv3.