Tobias Reinhard

Tobias Reinhard

he/they

Postdoc @ TU Darmstadt

About me

I’m a postdoc and software verification expert at the Software Technology Group, TU Darmstadt. My research focuses on automated reasoning, static analysis, and tool development for safety- and mission-critical C code. Notable projects include working with the CBMC development team at AWS (a bounded model checker for C/C++) on scaling bounded to unbounded verification. Also at AWS, I formally verified memory- and thread-safety of FreeRTOS’ multi-core scheduler. I have a strong development background in Rust and C++.

Tooling For Automated Reasoning About C (Under Development)

Deductive verification of C code is often more complex than writing the code itself. This is partly due to the inherent difficulty of verification, but also to the fact that state-of-the-art verifiers are not designed with usability in mind. Proof languages and automation have not kept pace with the advances seen in mainstream programming languages over recent decades. As a result, users must often spell out proof details that could, in principle, be inferred automatically.

To make verification more accessible, I am developing a new, ergonomic deductive verifier for C (based on separation logic). The current research focus is on automating reasoning about heap data structures, significantly reducing the manual overhead involved in specifying proof details.

Interfacing with Lean4: Automation inevitably comes at the cost of expressivity. To address this, the verifier will support integration with Lean4. When higher expressivity is required, users will be able to carry out specific subproofs in Lean, accepting the additional effort in exchange for its richer proof language and dependent type system.

Completeness Thresholds (Ongoing)

Besides building verifier, 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.

` `

Research Interests

My general research interests are:

Program VerificationAutomated Reasoning
Programming Languages & ToolingStatic Analysis
Separation LogicBounded & Unbounded Proofs
Incremental ComputingType Systems

Dissertation

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds, KU Leuven 2024
[Lirias (KU Leuven)] [arXiv]

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 modular approaches to scale CBMC 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:

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.