My research is about  Analysis and Verification: understanding software and specifications,
reasoning about them, proving that they satisfy desirable properties, showing that they behave correctly.

Common themes in my research are:

Security, Safety, Use of Information Theory, and Dependence Analysis

My current research interests include the following applications:

  • Program flow security
  • Slicing programs and software models
  • Semantics based malware detection
  • Software testing
  • Quantified information flow
More information about these research areas can be found in my published papers:


I am a member of  CREST

I am a member of the EPSRC College (since 2006 until the present day)


Security and Code Free one day workshop 6 April 2011

Formal Methods and UML

Research Projects:
  • Semantic Matching of Malware (SeMaMatch) (2013-2016) (GCHQ/EPSRC)
  • Reducing the Cost of Oracles in Testing (RECOST) (2011-2014) (EPSRC)
  • CREST Platform Grant (2009-2014) (EPSRC)
  • Slicing State Based Models [SLIM] (2008-2011) (EPSRC)
  • Quantified Information Flow for Process Algebras 2007-2009 (Royal Society)
  • Quantified Information Flow 2006-2009 (EPSRC)
  • An Operational Approach to the Measurement of Information Flow Quantity 2005 (EPSRC)

PhD students

I am currently looking for good quality PhD students. Funding is available for students of sufficiently high quality. Areas of interest include:

Secure Information Flow

A lot effort in making software secure goes into a kind of fire-fighting, i.e. discovering and closing vulnerabilities in code. However, even if all vulnerabilities have been eliminated, code still may not be secure. It may contain covert channels that allow attacks on confidentiality of information, integrity of information, and the privacy and anonymity of the user. Such covert channels leaking information may be within the logic of the program or be so-called side channels such as measuring execution times or heat dissipation over different runs. The challenge of constructing security critical code for contemporary software is enormous. Semantics based program analysis and type systems have a large role to play in guaranteeing end-to-end information security for networked systems.

Semantic Analysis of Found Code

Found code is code that the analyser did not write. It may be source code or binaries. The task is to understand what it does and the (common) motivation is defence against malicious behaviours. Techniques include reverse engineering, program analysis, testing, and use of SMT solvers. There are a whole range of problem domains in this area, for example malware classification and techniques for combatting packing, encryption and rewriting engines.

Testing Information Transformers

The hypothesis for this research is that the answers to some long standing questions in the theory of testing programs can be found or at least improved by viewing programs as transformers of information and using techniques from information theory and the measurement of information flow in programs to build an information theoretic theory of testing which answers questions such as the following. How do I select the test suite? When is it adequate? What does adequate mean in terms of information? How do I order the tests? There is a security aspect to this research. An improvement in testing generally will improve the fire fighting of vulnerabilities and exploits, particularly when harnessed with information about attack vector templates.

If you are interested in any of the research areas above, please contact me


Last modified: Wed Apr 24 15:44:19 BST 2013