Research Interests
I am interested in the application of tools and theory for the specification and verification of software. I am also interested in type safe code generation.
I am the author of Abductor, a shape analysis tool engineered to scale to millions of lines of code. The theory it is based on, developed from a concept with Dino Distefano, is described in Compositional Shape Analysis by means of BI-Abduction.
News
June 2011. Journal paper on using Bi-Abduction to create scalable shape analyses has been accepted for publication in the Journal of the ACM. Available from the publications page.
Dec 2009. Since October I have been working part-time for Monoidics Ltd, a technology transfer startup, where I serve as Chairman and founder. My academic appointment is also part-time, and still funded entirely by EPSRC, whose support is gratefully acknowledged.
Sep 2009. Final versions of two APLAS09 papers, on resource invariant synthesis and proving copyless message passing, are available from the publications page.
Jun 2009. A new video on fractional permissions was presented at the workshop in honor of Richard Bornat’s 65th birthday. My nephews love it.
Nov 2008. Final versions of two POPL09 papers, on compositional shape analysis and Classical BI, are available from the publications page.
Nov 2008. I will be on the PC of POPL 2010.
Sep 2008. SpaceInvader in THE press.
Sep 2008. I will be PC chair of the Symposium on Automatic Program Verification, APV 2009, Argentina, February 14-15, 2009.
Sep 2008. East London Massive has released SpaceInvader 1.0.
Software
Smallfoot: automatic verification in separation logic. The cousin SmallfootRG supports fine-grained concurrency. Another relative SLAyer is doing well at Microsoft, and there is a newly born cousin HeapHop. There is a separate page for Space Invader, where the sources of the bi-abductive prover can also be downloaded.
MetaOCaml: a multi-staged extension of OCaml.
Publications
Here is a complete list
Program Committees
+ APV 2009 (Chair)
+ HAV 2007 (Heap Analysis and Verification)
Links
I am also a member of the East London Massive.
