HOME | DEUTSCH | IMPRESSUM | KIT

Dr.-Ing. Daniel Wasserrab

photo

Contact

Email: >>please click this text<<

[ PGP ]

IPD Prof. Snelting

Room 022, Building 50.34

Am Fasanengarten 5

76131 Karlsruhe

Germany

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

2014

2010

2009

2008

2007

2006

2005

2004

Talks

  • Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing. VERIFY 2010, July 2010. Slides: Keynote, PDF
  • 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

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