Categories: research

Research

Introduction

I work on program verification, formal methods and theorem proving. In general, I am interested in what we can prove about the systems we can build, and what those proofs say about the systems we should build. My current focus is on:

reasoning directly with operational semantics (see publications)
weak memory
parsing
(verified) filesystems
tools to support formal definitions, Ott and Lem
verified computational complexity of real-world algorithm implementations
(staged) meta-programming

Please look at my publications and software

Past projects

2008-2009 Relaxed memory models, supervised by Matthew Parkinson of Microsoft Research, Cambridge (also in conjunction with Peter Sewell’s group).
2005-2008 NetSem project, formalizing TCP/IP, at the Computer Laboratory, University of Cambridge.