I am an Engineering Manager 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 currently runs in production analyzing every modification made to the code of Facebook’s mobile apps.

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.