|
|
|
Kontakt Tel.: +49 721 608-47401 Email:
Loading... |
IPD Prof. Snelting Raum 022, Gebäude 50.34 Am Fasanengarten 5 76131 Karlsruhe Deutschland |
|
Sprechzeiten: wann immer ich da bin / whenever I'm in my office |
|
Arbeitsgebiete
Interaktive Theorembeweiser, Programmverifikation
Lehre
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2022
- Vorlesung: Programmierparadigmen , Wintersemester 2021/2022
- Übung: Programmierparadigmen - Übungen , Wintersemester 2021/2022, Beste Übung
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2021
- Vorlesung: Programmierparadigmen , Wintersemester 2020/2021
- Übung: Programmierparadigmen - Übungen , Wintersemester 2020/2021
- Vorlesung: Programmierparadigmen , Wintersemester 2019/2020
- Übung: Programmierparadigmen - Übungen , Wintersemester 2019/2020
- Vorlesung: Semantik von Programmiersprachen , Sommersemester 2019
- Vorlesung: Programmierparadigmen , Wintersemester 2018/2019
- Übung: Programmierparadigmen - Übungen , Wintersemester 2018/2019, Beste Übung
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2018
- Vorlesung: Programmierparadigmen , Wintersemester 2017/2018
- Übung: Programmierparadigmen - Übungen , Wintersemester 2017/2018, Beste Übung
- Vorlesung: Semantik von Programmiersprachen , Sommersemester 2017
- Übung: Übungen zu Semantik von Programmiersprachen , Sommersemester 2017
Veröffentlichungen
2022
-
'do' Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)
Proc. ACM Program. Lang. August 2022 : S. Ullrich, L. d. Moura
2021
-
The Lean 4 Theorem Prover and Programming Language
Automated Deduction -- CADE 28 2021, pp. 625--635 : L. d. Moura, S. Ullrich
2020
-
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Automated Reasoning 2020, pp. 167--182 : S. Ullrich, L. d. Moura
2019
-
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming (Preprint)
31st symposium on Implementation and Application of Functional Languages September 2019 : S. Ullrich, L. d. Moura
2017
-
A Metaprogramming Framework for Formal Verification
Proc. ACM Program. Lang. September 2017 : G. Ebner, S. Ullrich, J. Roesch, J. Avigad, L. d. Moura
2016
-
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
Projekte
Betreute Studien- und Abschlussarbeiten
laufend
- Statische Einzigartigkeitsanalyse für Lean, Masterarbeit
abgeschlossen
- Eine Schnittstelle für Separation-Logic-Beweise in Lean, Masterarbeit
- Lokalisierung & Darstellung von lexikalischen Referenzen in einem Theorembeweiser, Bachelorarbeit
- Beweisvisualisierung für den Theorembeweiser Lean 4, Bachelorarbeit
- Diagrammjagd in einem interaktiven Theorembeweiser, Bachelorarbeit
- Formal verifiziertes Einfügen von Referenzzählungsinstruktionen, Bachelorarbeit
Bearbeitete Studien- und Abschlussarbeiten
- Formalisierung von SSA-Form (abgeschlossen), Bachelorarbeit
- Einfache Verifikation von Rust-Programmen (abgeschlossen), Masterarbeit