This website describes research activity in the southeast of England — at Imperial, UCL, Oxford, Cambridge University, Microsoft Research Cambridge and Queen Mary — on local reasoning about resources. It arose from work on various forms of separation logic and its associated automatic verification tools. The ongoing project is to develop an elegant theory (or theories) of resource reasoning that meshes with programmers' informal intuitions and leads to tractable analysis and verification techniques for a range of problem domains such as classic operating systems, the evolving world of web software and concurrent programming.

The research activity is underpinned by an EPSRC Programme Grant, ‘Resource Reasoning’, and also other grants, fellowships and industrial collaborations (see Support & Connections).