Note: I have recently moved offices, and am now in 202 (no longer 247)!
Teaching
Together with Henriette Färber I'm organising a lab course on interactive theorem proving using Isabelle/HOL in the winter 25/26 semester.
Open thesis/PdF topic offers can be found on the group's combined list.
Interests
- Formalisation of Mathematics and Logic in interactive theorem provers (such as Isabelle)
- Usable code extraction from from formally proven developments
- As part of the Convide Project I work on formalising consistency in model-driven engineering
Open invitation: Inspired by my former supervisor Lars Hupel, I offer an open invitation: if want to talk (or are curious) about any of the above topics, I want to talk to you! Feel free to send me an email, come to my office, or approach me at a conference or workshop.
If you're a student at KIT: if you're looking for a (Forschungspraktikum, PdF, ...) project or thesis touching on the above topics, feel free to reach out & let's talk about possibilities!
Publications
| Title | Author(s) | Source |
|---|---|---|
| Observable Semantics for Characterising Consistency Between Heterogeneous Models | Henriette Färber, Romain Pascual, Terru Stübinger, and Mattias Ulbrich | Software Engineering and Formal Methods (SEFM 2025) |
| Title | Author(s) | Source |
|---|---|---|
| Extending Isabelle/HOL's Code Generator with Support for the Go Programming Language | Terru Stübinger and Lars Hupel | 26th International Symposium on Formal Methods (FM 2024), Part II |
| Go Code Generation for Isabelle | Terru Stübinger and Lars Hupel | Archive of Formal Proofs |