Overview
My main area of research is semantics-based program analysis. This is a collection of techniques that may be used to infer dynamic properties of program behavior without running the program. The properties are approximated by simulating the program execution using simplified domains of values and techniques to ensure termination. Traditionally such techniques have been used in optimising compilers. The advantage of semantics-based techniques is that the analyses can be proved correct; in this context correctness is often called safety and guarantees that if the analysis infers a property then the program does really have that property.

Over the last few years it has become apparent that the same program analysis techniques can be used to certify programs against security criteria. We have worked on information flow analysis. We have also developed a new notion of approximate confinement which, recognising that perfect security may be unattainable, aims to quantify how vulnerable a system is.

My early work was based on qualitative approaches to program analysis using lattice and domain theory as a basis. Recently, together with Di Pierro and Wiklicky, I have been developing a framework for the quantitative analysis of programs and systems.