|
|
|
Kontakt |
IPD Prof. Snelting , Gebäude 50.34 Am Fasanengarten 5 76131 Karlsruhe Deutschland |
|
Sprechzeiten: nach Vereinbarung |
|
Arbeitsgebiete
Formale Semantik, Statische Programanalyse
Lehre
- Vorlesung: Praxis der Softwareentwicklung , Wintersemester 2018/2019
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2018
- Praktikum: Praxis der Softwareentwicklung - λ-IDE , Wintersemester 2017/2018
- Vorlesung: Praxis der Softwareentwicklung , Sommersemester 2017
- Vorlesung: Semantik von Programmiersprachen , Sommersemester 2017
- Übung: Übungen zu Semantik von Programmiersprachen , Sommersemester 2017
- Vorlesung: Praxis der Softwareentwicklung , Wintersemester 2016/2017
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2016, Bestes Praktikum
- Vorlesung: Praxis der Softwareentwicklung , Sommersemester 2015
- Übung: Übungen zu Semantik von Programmiersprachen , Sommersemester 2015
- Vorlesung: Praxis der Softwareentwicklung , Wintersemester 2014/2015
- Vorlesung: Praxis der Softwareentwicklung , Sommersemester 2014
- Vorlesung: Praxis der Softwareentwicklung , Wintersemester 2013/2014
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2013, Bestes Praktikum
- Vorlesung: Programmierparadigmen , Wintersemester 2012/2013
- Übung: Programmierparadigmen - Übungen , Wintersemester 2012/2013
- Vorlesung: Praxis der Softwareentwicklung , Sommersemester 2012
- Vorlesung: Praxis der Softwareentwicklung , Wintersemester 2011/2012
- Vorlesung: Praxis der Softwareentwicklung - SudoPhone: Sudoku für Smartphones mit Android , Wintersemester 2011/2012
- Vorlesung: Praxis der Softwareentwicklung - Smartphoneprogrammierung in Java , Sommersemester 2011
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2011
- Vorlesung: Praxis der Softwareentwicklung: TauchcomputerApp - Sicherheitskritische Software für Android , Wintersemester 2010/2011
- Seminar: Programmkalküle für Parallelität , Sommersemester 2010
- Vorlesung: Programmieren , Wintersemester 2009/2010
- Tutorium: Tutorien zu Programmieren , Wintersemester 2009/2010
- Übungsschein: Programmieren für Wiederholer , Sommersemester 2009
- Vorlesung: Programmieren , Wintersemester 2008/2009
- Tutorium: Tutorien zu Programmieren , Wintersemester 2008/2009
Veröffentlichungen
2018
-
Illi Isabellistes Se Custodes Egregios Praestabant
Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday 2018, pp. 267--282 : S. Bischof, J. Breitner, D. Lohner, G. Snelting
2017
-
Minimal Static Single Assignment Form
Archive of Formal Proofs January 2017 : M. Wagner, D. Lohner
2016
-
The meta theory of the Incredible Proof Machine
Archive of Formal Proofs May 2016 : J. Breitner, D. Lohner -
Verified Construction of Static Single Assignment Form
Archive of Formal Proofs February 2016 : S. Ullrich, D. Lohner -
Verified Construction of Static Single Assignment Form
25th International Conference on Compiler Construction 2016, pp. 67--76 (CC 2016) : S. Buchwald, D. Lohner, S. Ullrich
2010
-
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
-
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
Projekte
Betreute Studien- und Abschlussarbeiten
vergeben
- Programmieren-Tutor, HiWi-Job
- Softwaresicherheitsanalysen mit Isabelle/HOL, HiWi-Job
abgeschlossen
- Odyssee, HiWi-Job
- Call Arity vs. Demand Analysis, Masterarbeit
- Formalisierung von SSA-Form, Bachelorarbeit
- Verifizierte Implementierung von Patricia-Bäumen, Studienarbeit
- Formalisierung von SSA-Form, Masterarbeit
- Funktionale Summary-Kanten-Berechnung für PDGs , Bachelor-/Studienarbeit
- Verifizierte Berechnung von Datenabhängigkeiten, Bachelor-/Studienarbeit
- Verifizierte Berechnung von Kontrollabhängigkeiten, Bachelor-/Studienarbeit