|
|
|
Kontakt |
IPD Prof. Snelting Raum 022, Gebäude 50.34 Am Fasanengarten 5 76131 Karlsruhe Deutschland |
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
-
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
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
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2010
- Seminar: Programmkalküle für Parallelität , Sommersemester 2010
- Vorlesung: Theorembeweiser und ihre Anwendungen , Sommersemester 2009
- Übung: Übungen zu Theorembeweiser und ihre Anwendungen , Sommersemester 2009
- Übung: Übungen zu Fortgeschrittene Objektorientierung , Sommersemester 2008
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
- Teilnahme an der Summer School Marktoberdorf 2005 und der Midland Graduate School 2008
-
Meine Erdős Nummer
ist maximal 4 (und ziemlich sicher auch nicht kleiner):
Daniel Wasserrab -> Tobias Nipkow -> Gerhard Weikum -> Patrick Eugene O'Neil -> Paul Erdős