David Aspinall

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.

Together with Mike Just I have been working on studying new and current techniques for Knowledge-Based Authentication.

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.

The Mobility and Security Group is working on ideas for new projects. Our two main projects ended in 2009, these were:

• An EPSRC project: ReQueST
• An EU project: MOBIUS

ReQueST had an EPSRC-funded follow-on project called Resource Static Analysis building static analysis tools for Java programs to analyse and check their resource usage. This finished in 2010.

See some more of my past projects.