HOME | ENGLISH | IMPRESSUM | KIT

Dr.-Ing. Daniel Wasserrab

photo

Kontakt

Email: >>Bitte hier klicken<<

[ PGP ]

IPD Prof. Snelting

Raum 022, Gebäude 50.34

Am Fasanengarten 5

76131 Karlsruhe

Deutschland

Sprechzeiten: Do 10-11 Uhr

Arbeitsgebiete

Formale Semantik/Mehrfachvererbung
Ich habe eine formale Semantik einer C++-ähnlichen Sprache, gennant CoreC++, entwickelt. Diese Sprache ist eine Weiterentwicklung/Anpassung von Jinja, einer Java-ähnlichen Sprache, die am Lehrstuhl von Prof. Nipkow an der Technischen Universität München entwickelt wurde. Die Formalisierung und der Korrektheitsbeweis wurden im generischen Theorembeweiser Isabelle durchgeführt.

Verifikation von Slicing
Slicing mithilfe von Kontrollfluß- und Programmabhängigkeitsgraphen ist eine Standard-Programmanalyse. Diese sprachunabhängigen Graphstrukturen enthalten in Kombination mit gewissen Wohlgeformtheitsbedingungen genug Information um Slicing durchzuführen und zu verifizieren. Wir verifizieren, basierend auf diesen Strukturen, verschiedene Arten des Slicings: dynamisch, statisch intra- und interprozedural. Außerdem wollen wir zeigen wie verschiedene Semantiken (z.B. Jinja and CoreC++) in diese Strukturen eingebettet werden können, womit Slicing für die Kerne bekannter OO-Sprachen verifiziert wäre.

Veröffentlichungen

2014

2010

2009

2008

2007

2006

2005

2004

Vorträge

  • Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing. VERIFY 2010, Juli 2010. Folien: Keynote, PDF
  • On PDG-Based Noninterference and its Modular Proof. PLAS 2009, Juni 2009.
  • Korrektheitsbeweise für IFC mittels des Theorembeweisers Isabelle/HOL. GI FOMSESS Treffen 2009, März 2009.
  • C++ ist typsicher? Garantiert! Eingeladener Vortrag auf der SE 2007, März 2007 und TU Berlin, Juni 2007.
  • An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++. OOPSLA 2006 und IBM, Oktober 2006.

Projekte

Lehre

Frühere Lehrveranstaltungen (Universität Passau)

  • Vorlesung "Theorembeweiser und ihre Anwendungen" SS 07
  • Übung zu "Objektorientierte Programmierung" WS 06/07, WS 07/08
  • Hauptseminar Softwaretechnik WS 05/06, SS 06, WS 06/07
  • Korrektur von Programmieraufgaben in Programmieren II/Praxis des Programmierens
  • Übung "Algorithmen und Datenstrukturen" SS 06

Studentenprojekt

CyBaL: eine C++ Bibliothek mit verschiedenen Algorithmen zur Bestimmung der minimalen Kreisbasis eines Graphen.

Verschiedenes