Tobias Reinhard

Tobias Reinhard

Postdoc @ TU Darmstadt

About me

I’m a postdoctoral researcher at the Software Technology Group, TU Darmstadt. My research focuses on automated reasoning, neuro-symbolic AI, software verification, static analysis, and tool development, with past projects targeting 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, Python and C++.

Neuro-symbolic AI for Code Reasoning

In recent years, we’ve seen remarkable advances in generative AI through large language models (LLMs). They are capable of writing code, mimicking human reasoning processes and making complex decisions. Yet, they severely suffer from hallucinations, i.e., producing reasonably seeming but incorrect results, which diminishes their reliability in critical fields like program verification and analysis.

To address this, my research focuses on combining neural and symbolic approaches to reasoning about code. By integrating LLMs with formal verification techniques, I aim to make AI-driven reasoning both intelligent and verifiable, and ultimately to make formal verification scalable.

LLM-First Verification-Aware Programming Language

Generating provably correct code with LLMs is a promising direction for eliminating entire classes of bugs and vulnerabilities. LLMs often get the high-level proof intuition right, but struggle with low-level details. A key reason is that in existing verifiers, source-level control flow does not align with the underlying proof structure, hiding relevant learning signals from the model.

To this end, I am developing a verification-aware programming language built around this insight: one where control flow is aligned with the proof tree, and reasoning happens at a coarse-grained level that matches how LLMs naturally operate. The goal is to maximize the learning signal available to the model while minimizing the proof burden, making provably correct code generation a practical reality.

Completeness Thresholds

In the past, I also worked on completeness thresholds for memory safety proofs. The goal of this work was to reduce unbounded memory safety proofs to bounded ones.

` `

Research Interests

My general research interests are:

Neuro-Symbolic AIAutomated Reasoning
Verifier-Guided Reinforcement-LearningSoftware Verification
Agentic AIProgramming Languages & Tooling

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.