Coordinates
Chair of Software Engineering
University of Freiburg
Georges-Köhler-Allee 52
D-79110 Freiburg im Breisgau
Germany
building, room
052-00-022
+49 761 203 8291 (phone)
+49 761 203 8242 (fax)
Research Interests
Program analysis and verification, shape analysis, automated abstraction, abstraction refinement, applications of automated reasoning.
One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. State-of-the-art software model-checkers are very successful in analyzing control-intensive software such as device drivers, but they are limited when it comes to programs that make heavy use of data structures and whose correctness depends on complex consistency properties of these data structures. In my Ph.D. research I am developing software model-checking algorithms that are applicable to this domain of programs.
Publications
- Heap Assumptions on Demand with Andreas Podelski and Andrey Rybalchenko
In Proceedings of CAV, 2008. [pdf] [pdf-extended] - Shape analysis for composite data structures with Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, and Hongseok Yang
In Proceedings of CAV, 2007. [pdf] - Verifying Complex Properties using Symbolic Shape Analysis with Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard
Workshop on Heap Abstraction and Verification, March 2007. [pdf] - Using First-Order Theorem Provers in the Jahob Data Structure Verification System with Charles Bouillaguet, Viktor Kuncak, Karen Zee, and Martin Rinard
In Proceedings of VMCAI, 2007. [pdf] - Field Constraint Analysis with Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard
In Proceedings of VMCAI, 2006. [pdf] [pdf-extended] [pdf-slides] - Boolean Heaps with Andreas Podelski
In Proceedings of SAS, 2005. [pdf] [pdf-slides] - Symbolic Shape Analysis
Diploma Thesis, Saarland University, Saarbrücken, Germany, September 2004. [pdf]
Tools
Teaching
- Tutorials for the lecture Verification, winter term 2004/05 at Saarland University
- Tutorials for the lecture Formal Methods for Java, summer term 2007
- Seminar on Advanced Topics in Model-Checking, summer term 2008