Contact Email:
Bitte warten... [ PGP ] 
IPD Prof. Snelting Room 022, Building 50.34 Am Fasanengarten 5 76131 Karlsruhe Germany 
Consultation Hours: Do 1011 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 Javalike 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 wellformedness 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 wellknown
objectoriented languages.
Publications
2014

Checking Probabilistic Noninterference Using JOANA
it  Information Technology November 2014, pp. 280287 : 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 MachineChecked
Correctness Proof for Slicing
6th International Verification Workshop  VERIFY2010 2010 : D. Wasserrab, D. Lohner
2009

Backing up Slicing: Verifying the Interprocedural TwoPhase HorwitzRepsBinkley
Slicer
Archive of Formal Proofs November 2009 : D. Wasserrab 
On PDGBased Noninterference and its Modular Proof
Proceedings of the 4th Workshop on Programming Languages and Analysis for Security June 2009, pp. 3144 : 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. 294309 (TPHOLS 2008) : D. Wasserrab, A. Lochbihler
2007

C++ ist typsicher? Garantiert!
Software Engineering 2007 March 2007, pp. 2931 : 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 ObjectOriented Programming, Systems, Languages, and Applications October 2006, pp. 345362 : 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 MachineChecked Correctness Proof for Slicing. VERIFY 2010, July 2010. Slides: Keynote, PDF
 On PDGBased 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
 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