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
- Emptieness 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.
- Verification, 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, submitted.
- Abstract Threads, VMCAI 2010, Madrid, Springer.
- 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.
Tools
- AMTV: Automated Modular Thread Verifier. Checks safety of multithreaded programs. Licence: GPLv3.