I'm a member of the Laboratory for Foundations of Computer Science (LFCS) and the Mathematical Reasoning Group. I'm also part of the wider collaboration of researchers in Informatics working on Security and Privacy.
My interests include:
For more details, please see my papers.
New! April 2013: We are starting an exciting new project on mobile application security called App Guarden. We looking for researchers and PhD students, please contact me if you are interested.
Advertisement: Come to CICM 2013, the amalgamated Conferences on Intelligent Computer Mathematics. It is in Bath, UK, 8-12 July 2013. Submissions and applications are still open for workshops and the doctoral programme.
The Mobility and Security Group works on verification and certification techniques for establishing security and correctness of code, in particular, code for mobile and embedded devices. We have particular expertise in certification for resource limits, to show that programs and systems do not exceed bounds in resources such as time, memory, network bandwidth, and so on. Our new project App Guarden combines our expertise with colleagues from compilers and machine learning, to build a research secure application store.
Together with Mike Just I have been working on studying new and current techniques for Knowledge-Based Authentication and recently on passwords.
Proof General provides generic proof development environments for Isabelle, Coq, and other theorem provers. Connected with the Proof General project, I am conducting research into Proof Engineering and Hierarchical Tactic Languages.
I am a co-Investigator on the EPSRC Platform Grant The Integration and Interaction of Multiple Mathematical Reasoning Processes held in the Mathematical Reasoning Group which is conducting a range of innovative work connected with automated and interactive theorem proving. We recently completed an award that funded a visiting mathematician to work on formalising some new parts of mathematics inside Isabelle, in a grant entitled The potential of automated reasoning tools to assist the working mathematician.
See some more of my past projects.