About me
I’m a postdoc and software verification expert at Software Technology Group, TU Darmstadt working on verification techniques for imperative, heap-manipulating programs. My overall goal is to simplify program verification. I recently completed my PhD on liveness verification and completeness thresholds under the supervision of Bart Jacobs.
Dissertation
Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds, KU Leuven 2024
[Lirias (KU Leuven)] [arXiv]
Completeness Thresholds
My current research focuses on completeness thresholds for memory safety proofs. The goal of this work is to reduce unbounded memory safety proofs to bounded ones.
- Completeness Thresholds for Memory Safety of Array Traversing Programs, SOAP 2023
[Paper ACM / arXiv] [Technical Report] [Bibtex] - Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
- Poster, SPLASH 2023 [Zenodo]
- Extended Abstract [arXiv]
- Invited talks on completeness thresholds:
- Programming Technology Group @ University of Oslo, [Slides] May 2024
- Programming Languages and Verification Seminar @ Portland State University [Slides], November 2023
- Programming Group @ HSG, St Gallen [Slides], October 2023
Research Interests
My general research interests are:
| Program Verification | Automated Reasoning |
| Separation Logic | Bounded & Unbounded Proofs |
| Programming Languages | Type Systems |
| Static Analysis | Reversible Programming |
AWS
In autumn 2022 and summer 2021, I worked as applied scientist intern with Mark Tuttle in the Automated Reasoning Group at Amazon Web Services.
During my 2022 internship I verified the multicore implementation of the FreeRTOS scheduler, identified a buffer underflow, proposed a fix and proved that it works.
FreeRTOS is a state-of-the-art real-time operating system for embedded systems that runs on many IoT devices. Originally it had been developed for single-core platforms and is currently being ported to multi-core. Using VeriFast, a deductive verifier for C based on separation logic, I proved the scheduler to be memory and thread safe, once my fix has been applied. The proof is an unbounded proof, that is, the provided guarantees hold for all possible interleavings and no matter how big the involved data structures are.
During my 2021 internship I explored ways to progress from bounded to unbounded verification. My research focused on (automatic) memory safety proofs for heap-manipulating programs that involve inductive data structures. I worked on separation-logic based deductive verification as well as on a research prototype that’s based on a mixture of automatic axiom instantiation and term rewriting.
Liveness
During my previous research project, I developed a separation logic to verify liveness properties of concurrent programs:
Ghost Signals: Verifying Termination of Busy Waiting, CAV 2021
[Paper] [Extended Version] [TR] [Bibtex]A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit, FTfJP 2020
[Paper] [TR] [Bibtex] [Slides]
Before my PhD
Before I joined DistriNet, I obtained my Master’s degree from TU Darmstadt. During my Master’s I worked as student research assistant at the Software Technology Group on type systems for multitier-languages such as ScalaLoci.