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.



Deep Program Understanding

Established: June 1, 2015

We aim to teach machines to understand complex algorithms, combining methods from the programming languages and the machine learning communities. Learning Algorithms A core problem of machine learning is to learn algorithms that explain observed behavior. This can take several forms, such as program synthesis from examples, in which an interpretable program matching given input/output pairs has to be produced; or alternatively programming by demonstration, in which a system has to learn to mimic sequences…











T2 Temporal Prover

October 2014

T2 is designed to prove safety and liveness properties of programs, expressed as reachability, termination, or in the temporal logic CTL. Also see, https://github.com/mmjb/T2.

Size: 10 MB

    Click the icon to access this download

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