Longer Bio

I'm a researcher at Meta AI and a Professor at University College London. I've done research in the broad areas of programming languages and logic, and held academic positions at Syracuse University, Queen Mary University of London, and University College London. I worked at Facebook from 2013-2021 after the acquisition of a verification startup Monoidics I cofounded. I moved to Lacework where I founded their Code Security team, which released a suite of products in 2023. Lacework was acquired by Fortinet in 2024. I then moved back to Meta, this time to work in the FAIR (Fundamental AI Research) team.

My research has involved development of new logics and automated tools based on them. With David Pym, I developed Bunched Logic, a general logic of resources. BI was then used in Separation Logic, developed in joint work with John Reynolds and others, a theory which opened up new practical possibilities for program proof, including the technology which led to the Infer program analyzer developed by my team at Facebook. Infer runs internally on Facebook's code bases, and has detected hundreds of thousands of bugs which have been fixed by Facebook's developers before reaching products. Infer is also used in production at number of other companies, including Amazon, Microsoft and Mozilla, and is deployed to many other organizations through the Sonatype Lift analysis platform. Most recently I developed Incorrectness Logic, a theory aimed at providing a foundation for bug catching tools based on proofs of the presence of bugs.

I'm a Fellow of the Royal Society (elected 2018), a Fellow of the Royal Academy of Engineering (2016), have received a number of awards including the the 2016 G\"odel Prize, the 2016 CAV Award, the 2021 IEEE Cybersecurity Award for Practice, and test-of-time awards for papers in POPL (2001 and 2009 papers) and CONCUR (2004 paper). I received an honorary doctorate from Dalhousie University in 2018, the same university where I got my BSc in 1985.