Lehrstuhl Programmierparadigmen Logo Dipl.-Inf. Univ. Daniel Wasserrab
photo
Contact
Phone: +49 721 608-7399
E-Mail: [ PGP ]
Address
IPD Prof. Snelting
Room 022
Adenauerring 20a
76131 Karlsruhe
Consultation Hours
Do 10-11 Uhr

Research interests

Formal semantics/Multiple inheritance
I finished a formal semantic of a C++-like language, called CoreC++. This language is based on Jinja, a Java-like language, developed by the group of Prof. Nipkow at the Technische Universitaet Muenchen. The formalization and proof of correctness is performed in the generic proof system Isabelle.

Verification of Slicing
Slicing, basing on control flow and program dependence graphs, is a standard program analysis. These language independent graph structures, together with certain well-formedness conditions, contain enough information to perform and verify slicing. We verify various kinds of slicing (dynamic and static intra- as well as static interprocedural) based on these structures. Furthermore we aim to show how different language semantics (e.g. Jinja and CoreC++) can be embedded in these structures, thus verifying slicing for the cores of well-known object-oriented languages.

Publications

2009
D. Wasserrab : Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer. AFP 2008
D. Wasserrab, D. Lohner, G. Snelting : On PDG-Based Noninterference and its Modular Proof. PLAS 2009
2008
G. Snelting, D. Wasserrab : A Correctness Proof for the Volpano/Smith Security Typing System. AFP 2008
D. Wasserrab : Towards Certified Slicing. AFP 2008
D. Wasserrab, A. Lochbihler : Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. TPHOLS 2008
2007
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip : C++ ist typsicher? Garantiert!. SE 2007
2006
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip : An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++. OOPSLA 2006
D. Wasserrab : CoreC++. AFP 2006
2005
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip : An Operational Semantics and Type Safety Proof for C++-like Multiple Inheritance. TechReport
2004
D. Wasserrab : Formale Semantik einer C++-ähnlichen Sprache mit Fokussierung auf Mehrfachvererbung.

Talks

  • On PDG-Based Noninterference and its Modular Proof. PLAS 2009, June 2009.
  • Korrektheitsbeweise für IFC mittels des Theorembeweisers Isabelle/HOL. GI FOMSESS Meeting 2009, March 2009.
  • C++ ist typsicher? Garantiert! Invited Talk at SE 2007, March 2007 and TU Berlin, June 2007.
  • An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++. OOPSLA 2006 and IBM, October 2006.

Projects

Advised thesis subjects

Courses

Former Courses (University of Passau)

  • Lecturer of "Theorem provers and their applications" SS 07
  • Tutorial "Advanced Object Oriented Programming" WS 06/07, WS 07/08
  • Graduate seminar Software Technology WS 05/06, SS 06, WS 06/07
  • Correcting programming exercises in Programming II/PDP
  • Tutorial "Algorithms and Datastructures" SS 06

Student Project

CyBaL: a C++ library including various algorithms for finding minimal cycle bases of graphs.

Misc