Dr.-Ing. Daniel Wasserrab

	Contact	IPD Prof. Snelting Room 022, Building 50.34 Am Fasanengarten 5 76131 Karlsruhe Germany

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

• Checking Probabilistic Noninterference Using JOANA
  it - Information Technology November 2014, pp. 280--287 : G. Snelting, D. Giffhorn, J. Graf, C. Hammer, M. Hecker, M. Mohr, D. Wasserrab

2010

• From Formal Semantics to Verified Slicing - A Modular Framework with Applications in Language Based Security
  October 2010 : D. Wasserrab
• Information Flow Noninterference via Slicing
  Archive of Formal Proofs March 2010 : D. Wasserrab
• Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
  6th International Verification Workshop - VERIFY-2010 2010 : D. Wasserrab, D. Lohner

2009

• Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
  Archive of Formal Proofs November 2009 : D. Wasserrab
• On PDG-Based Noninterference and its Modular Proof
  Proceedings of the 4th Workshop on Programming Languages and Analysis for Security June 2009, pp. 31--44 : D. Wasserrab, D. Lohner, G. Snelting

2008

• A Correctness Proof for the Volpano/Smith Security Typing System
  Archive of Formal Proofs September 2008 : G. Snelting, D. Wasserrab
• Towards Certified Slicing
  Archive of Formal Proofs September 2008 : D. Wasserrab
• Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
  Proceedings of the 21st International Conference of Theorem Proving in Higher Order Logics August 2008, pp. 294--309 (TPHOLS 2008) : D. Wasserrab, A. Lochbihler

2007

• C++ ist typsicher? Garantiert!
  Software Engineering 2007 March 2007, pp. 29--31 : D. Wasserrab, T. Nipkow, G. Snelting, F. Tip

2006

• An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++
  21th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications October 2006, pp. 345--362 : D. Wasserrab, T. Nipkow, G. Snelting, F. Tip
• CoreC++
  Archive of Formal Proofs May 2006 : D. Wasserrab

2005

• An Operational Semantics and Type Safety Proof for C++-like Multiple Inheritance
  2005 : D. Wasserrab, T. Nipkow, G. Snelting, F. Tip

2004

• Formale Semantik einer C++-ähnlichen Sprache mit Fokussierung auf Mehrfachvererbung
  2004 : D. Wasserrab

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

• Quis-Custodiet
• CoreC++

Courses

• Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2010
• Seminary: Programmkalküle für Parallelität , Sommersemester 2010
• Lecture: Theorem provers and their applications , Sommersemester 2009
• Common Excercises: Theorem provers and their applications - exercises , Sommersemester 2009
• Common Excercises: Übungen zu Fortgeschrittene Objektorientierung , Sommersemester 2008

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

• Participation in Summer School Marktoberdorf 2005 and Midland Graduate School 2008
• My Erdős number is at most 4 (and most likely not smaller than this):
  Daniel Wasserrab -> Tobias Nipkow -> Gerhard Weikum -> Patrick Eugene O'Neil -> Paul Erdős