About

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.

 

Publications

2016

2015

2014

2013

2012

2011

2010

Other

Tools

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

Students

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.