Research

Hi! I'm Thomas (or just Tom) and I'm a doctoral student in the Programming Methodology group at ETH Zurich.

Blog

Check out my latest blog posts on various research topics.

Go to blog

OPLSS 2026

I'm going to OPLSS 2026! What I'm excited about.

Go to topic

About me and my research

I'm a doctoral student in the area of program verification. My research focuses on deductive verification of Unsafe Rust and how we can efficiently verify code that uses both, Safe and Unsafe Rust, by considering the constraints of the Safe Rust code that are enforced by the Rust type system. The developer should only have to add as little annotations as possible for proving safety of the Unsafe Rust parts of the code.

My background

Education

Direct Doctorate (MSc + PhD)
Computer Science; currently in Doctorate part
MSc GPA: 5.91/6.0
ETH Zurich
Zurich, Switzerland
09/2023 - expected 2029
Bachelor of Science
Software and Information Engineering
BSc GPA: 1.02/5 (lower is better)
TU Wien (Vienna University of Technology)
Vienna, Austria
10/2020 - 06/2023
HTL Matura
Dep.: Information Technology; Specialization: Networking Technology
GPA: 1/5 (lower is better)
HTL Wien 3 Rennweg
Vienna, Austria
09/2015 - 06/2020

Research experience

Master Thesis
ETH Zurich
02/2025 - 09/2025
  • Verification of the F-PKI Go implementation
  • Using the Gobra verifier
  • Access thesis
Research in CS
ETH Zurich
09/2024 - 01/2025
  • Elective course of my master's curriculum
  • Collecting bugs from bug trackers. Learning their syntactical left-most derivations using the grammar. Generate new bugs using what was learned from existing bugs.
Practical Work
ETH Zurich
09/2023 - 12/2023
  • Extending compiler testing project from Bachelor Thesis (see below)
  • Generalize approach by directly transforming source code files instead of generating SMT formulas and inserting them into code.
Bachelor Thesis
TU Wien
03/2023 - 06/2023
  • Extending compiler testing project from SSRF (see below)
  • In collaboration with the Advanced Software Technologies Lab at ETH Zurich
Scientific Research and Writing
TU Wien
10/2022 - 01/2023
  • Seminar paper in a course of my bachelor's curriculum
  • Summarizing how normative concepts (e.g. obligation) can be formalized in logic programming
Student Summer Research Fellowship (SSRF)
ETH Zurich
07/2022 - 08/2022
  • Highly-selective (2400 applicants world-wide; 19 taken)
  • Participants work in a research group
    • In my instance: Advanced Software Technologies Lab
  • My Project:
    • How stable are compilers when it comes to semantics-preserving transformations of dead if expressions (that were translated from unsat SMT formulas)?
    • Can compilers detect dead code when they were able/unable before the transformation?
    • Found various missed optimization opportunities in GCC and LLVM thanks to these observations
      • Some of them have already been fixed