I’m a Researcher at Microsoft Research in the Programming Principles and Tools group in Cambridge.
My research focuses on topics around software developer productivity. This includes fully automatic analyses of implicitly specified properties (such as memory safety, termination or complexity) and the use of machine learning techniques to help where classical program analysis fails. Most recently, I’ve also returned to some of my F/OSS roots and started studying the efficient use of build systems with colleagues in MSR and TSE.
I obtained my PhD at RWTH Aachen under the supervision of Jürgen Giesl, where I worked on termination and complexity analysis of (Java) programs. There, I focused on heap abstractions in the analysis of object-oriented programs, and details can be found on my old website.
My work has lead to a number of (publicly available) tools:
- A heap shape and termination analysis for heap-manipulating programs is implemented in AProVE (cf. the evaluations for Java and LLVM programs).
- Termination analysis for integer programs is implemented in T2, successor to the original TERMINATOR project (cf. evaluation).
- Complexity analysis for integer programs is implemented in KoAT (cf. evaluation) and LoAT (cf. evaluation)
- Verification of CTL properties with first-order quantification is implemented in CTLFO (cf. evaluation).