I am a Research Scientist working with the Static Analysis Tools team in the Facebook London Engineering office. I came to Facebook in 2013 with the acquisition of the verification startup Monoidics, and before that I held academic positions at Syracuse University, Queen Mary University of London and University College London. I maintain a part-time Professor position at UCL.

My research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of formal proof. With John Reynolds I developed separation logic, a theory which opened up new practical possibilities for program verification. Subsequent work in academic program analysis eventually led to the the Monoidics/Facebook Infer program analyzer, which is notable for supporting deep reasoning about big code that is undergoing rapid concurrent modification. Infer currently runs in production at Facebook, where it helps thousands of bugs be fixed each month before reaching production.

I have received a number of awards for my work in verification including the 2016 CAV Award and the 2016 Godel Prize. I was elected fellow of the UK Royal Academy of Engineering in 2016.

Links

Publications

Blog