Philipp Körner
Kontakt
Heinrich-Heine-Universität Düsseldorf
Institut für Informatik
Universitätsstraße 1
D-40225 Düsseldorf
Email:
Tel.: +49 (211) 81-10713
Fax: +49 (211) 81-10712
Raum: 25.12.02.56
Meine Forschungsinteressen
- Model Checking / Sicherheitskritische Systeme
- Performance und Optimierungen
- Verwendung von formalen Spezifikationen zur Laufzeit
- hybrides Model Checking
- Funktionale / Logische Programmierung
- Typsysteme, Test-Case Generation (vgl. plspec)
- Blockchains
- Analyse und Verifikation von Smart Contracts
Aktuelle Lehrveranstaltungen (Sommersemester 2022)
- Vertiefung Funktionale Programmierung: Clojure
Frühere Lehrveranstaltungen
- Einführung in die Funktionale Programmierung (Wintersemester 2021/22, Inverted Classroom)
- Vertiefung Funktionale Programmierung: Clojure (Sommersemester 2021, Seminar)
- Funktionale Programmierung (Wintersemester 2020/21, Inverted Classroom)
- Model Checking (Sommersemester 2020, Inverted Classroom)
- Funktionale Programmierung (Wintersemester 2019/20, Übung)
- Seminar Blockchain (Sommersemester 2019)
- Vertiefung logische Programmierung (Sommersemester 2019, Übung)
- Funktionale Programmierung (Wintersemester 2018/19)
- Model Checking (Sommersemester 2018)
- Funktionale Programmierung (Wintersemester 2017/18)
- Theoretische Informatik (Organisation u. Übung, Sommersemester 2017)
- Funktionale Programmierung (Übung, Wintersemester 2016/17)
- Funktionale Programmierung (Übung, Wintersemester 2015/16)
Abschlussarbeiten
Die folgenden Abschlussarbeiten habe ich (mit-)betreut:
Name | Titel | Art |
---|---|---|
Gesine Pfeil | Visualization of Clojure Data Structure | Bachelorarbeit |
Sebastian Stock | Ein Cloud Controller für verteiltes Modelchecking | Bachelorarbeit |
Isabel Wingen | An Optional Type System for Prolog | Projektarbeit |
Sarah Glasmacher | Embedding Differential Equations into ProB | Bachelorarbeit |
Isabel Wingen | You're Not My Type: Analyzing Prolog Programs | Masterarbeit |
Sebastian Sura | Eine Paketverwaltung für Prolog | Bachelorarbeit |
Maximilian Bauer | An Improved CSP Interpreter for ProB | Masterarbeit |
Jan Roßbach | Boolean Encoding of Statically Finite Sets in B Machines | Bachelorarbeit |
Offenen Themen für Abschlussarbeiten finden Sie hier.
Veröffentlichungen
2024
- A verified low-level implementation and visualization of the adaptive exterior light and speed control system.In International Journal on Software Tools for Technology Transfer, 2024.
- The final authenticated version is available online at https://doi.org/10.1007/s10009-024-00750-5
- Meta-Programming Event-B — Advancing Tool Support and Language Extensions.In Proceedings ABZ (International Conference on Rigorous State-Based Methods), Lecture Notes in Computer Science, 14759, Springer, 233--240, 2024.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-63790-2_17
2023
- On Executing State-Based Specifications and Partial Order Reduction for High-Level Formalisms.PhD Thesis, Heinrich-Heine-Universität, Düsseldorf, Germany, 2023.
- The final authenticated version is available online at https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=61784
2022
- Fifty Years of Prolog and Beyond.In Theory and Practice of Logic Programming, 22, 6, 776--858, 2022.
- The final authenticated version is available online at https://doi.org/10.1017/S1471068422000102
- An embedding of B in Clojure.In Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, MODELS 2022, Montreal, Quebec, Canada, October 23-28, 2022, ACM, 598--606, 2022.
- The final authenticated version is available online at https://doi.org/10.1145/3550356.3561561
- Towards Practical Partial Order Reduction for High-Level Formalisms.In Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Revised Selected Papers, Lecture Notes in Computer Science, 13800, Springer, 72--91, 2022.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-25803-9_5
2021
- Rooting Formal Methods within Higher Education Curricula for Computer Science and Software Engineering -- A White Paper.In CCIS, 1301, Springer, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-71374-4_1
- LINK
- Prototyping Games Using Formal Methods.In Proceedings FMFun 2019, CCIS, 1301, Springer, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-71374-4_6
2020
- A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System.In Proceedings ABZ, LNCS, 12071, Springer, 2020.
- The final authenticated version is available online at https://link.springer.com/chapter/10.1007/978-3-030-48077-6_30
- Towards a Shared Specification Repository.In Proceedings ABZ, LNCS, 12071, Springer, 2020.
- The final authenticated version is available online at https://link.springer.com/chapter/10.1007/978-3-030-48077-6_22
2019
- Measuring Coverage of Prolog Programs Using Mutation Testing.In Proceedings WFLP 2018, LNCS, 11285, Springer, 2019.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-16202-3_3
- Embedding High-Level Formal Specifications into Applications.In Proceedings FM, LNCS, 11800, Springer, 2019.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-30942-8_31
- A Multi-Target Code Generator for High-Level B.In Proceedings iFM, LNCS, 11918, Springer, 2019.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-34968-4_25
2018
- plspec - A Specification Language for Prolog Data.In Proceedings Declare 2017, Dietmar Seipel and Michael Hanus and Salvador Abreu, LNAI, 10997, Springer, 2018.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-00801-7_13
- Three is a crowd: SAT, SMT and CLP on a chessboard.In Proceedings PADL 2018, LNCS, 10702, Springer, 2018.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-73305-0_5
- Distributed Model Checking Using ProB.In Proceedings NFM 2018, LNCS, 10811, Springer, 2018.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-77935-5_18
- State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin.In Proceedings iFM 2018, LNCS, 11023, Springer, 2018.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-98938-9_16
- Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains.In Proceedings ABZ 2018, Michael Butler and Alexander Raschke and Thai Son Hoang and Klaus Reichl, LNCS, 10817, Springer, 292--306, 2018.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-91271-4_20
2016
- Symbolic Reachability Analysis of B through ProB and LTSmin.In Proceedings iFM 2016, LNCS, 9681, Springer, 2016.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-33693-0_18