David Aspinall's Home Page

Research
Teaching
Commercial
Admin
Other

Research

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:

software security: certified security and proof-carrying code
user authentication: passwords and challenge questions
theorem proving: proof development environments and proof language foundations
programming and specification languages: type systems and modules

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.

Research Projects

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.

Research Students

Current students:

Daniel Franzen, working on software security for mobile applications. Daniel was the first signed up member of the App Guarden project.
Iain Whiteside, working on proof development techniques. Iain's work is co-supervised with Gudmund Grov and before that with Lucas Dixon.
Gavin Keighren working on security APIs. Gavin's work is co-supervised with Graham Steel.

If you're interested in studying for a PhD, drop me a line to discuss topics and check the Informatics PG page and the LFCS PG page. I will supervise students within my areas of interest,

Former students:

Jaroslav Sevcik, whose PhD thesis Program Transformations in Weak Memory Models was examined in December 2008.
Robert Atkey, whose PhD thesis Substructural Simple Type Theories for Separation and In-place Update was examined in November 2005.

David R. Aspinall, email david.aspinall@ed.ac.uk.
Contact GPG key (Instant HOWTO)