I’m a Researcher at Microsoft Research in the Machine Intelligence and Perception and Programming Principles and Tools groups 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 of my recent work was done in the context of the Deep Program Understanding project.

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).


I had the pleasure of working with a bunch of bright students as interns: Yuxin ChenJack Feser, Alex Gaunt, Maria GorinovaSid Krishna, Wing Lam, Yujia LiRenjie Liao, He Zhu.