Research
My research focuses on AI-assisted software verification and debugging. It builds on my work in software engineering, software verification, and machine learning, with an emphasis on investigating program behavior and reasoning about correctness.
AI-assisted Software Verification and Debugging
My current DFG Walter Benjamin project at Humboldt-Universität zu Berlin is SDECOPILOT: Assisting Developers in Building Correct Software with Debugging Agents.
The project explores how AI can assist developers in understanding program behavior, finding bugs, and assessing possible repairs. It aims to combine AI-based approaches with established methods of software analysis and verification to support reasoning about program correctness.
Neural Bug Detection
I have investigated how machine learning models can learn from developer mistakes to detect and repair software bugs.
This includes work on training neural bug detectors with artificial and real-world bugs, as well as the development of RealiT.
This work examines how training data affects bug detection and compares neural detectors with developers on variable misuse bugs. The TSSB-3M dataset provides mined single-statement bugs for studying these questions.
Selected publications:
- How to Train Your Neural Bug Detector: Artificial vs Real Bugs (ASE 2023)
- Are Neural Bug Detectors Comparable to Software Developers on Variable Misuse Bugs? (ASE 2022)
- Learning Realistic Mutations: Bug Creation for Neural Bug Detectors (ICST 2022)
- TSSB-3M: Mining Single Statement Bugs at Massive Scale (MSR 2022)
Cooperative Software Verification
Another focus of my research is improving automated software verification by combining and coordinating different verification techniques.
Our ICSE 2025 work investigates dynamic program splitting: dividing a verification task into smaller programs on demand and coordinating existing verifiers to analyze them. Related work studies how to construct verifier combinations from existing components and how to parallelize analysis by splitting program paths into ranges.
My work includes verification tools such as PeSCo-CPA and BubaaK-SpLit.
These tools achieved third place in the ReachSafety category at SV-COMP 2019 and second place in the SoftwareSystems category at SV-COMP 2024, respectively.
Selected publications:
- Cooperative Software Verification via Dynamic Program Splitting (ICSE 2025)
- Construction of verifier combinations from off-the-shelf components (Formal Methods in System Design, 2025)
- BUBAAK: Dynamic Cooperative Verification (TACAS 2025)
- Parallel program analysis on path ranges (Science of Computer Programming, 2024)
- Bubaak-SpLit: Split what you cannot verify (TACAS 2024)
- PeSCo: Predicting Sequential Combinations of Verifiers (TACAS 2019)
Learning-Based Methods and Formal Verification
I also investigate how learning-based systems and formal verification techniques can complement each other.
Published work includes learning to select verification algorithms from program representations and studying whether ChatGPT can propose loop invariants that established verification tools can check.
Selected publications:
- Can ChatGPT support software verification? (FASE 2024)
- Attend and Represent: A Novel View on Algorithm Selection for Software Verification (ASE 2020)
- Algorithm selection for software validation based on graph kernels (Automated Software Engineering, 2020)
Testing Software Verification Tools
Verification tools themselves need testing. Our work on robustness testing examines how changes that preserve a program’s semantics affect verifier results, helping identify weaknesses in verification tools.
Selected publication: