Research

The Institute builds on the work of the previous Institute in Automated Program Analysis and Verification (RIAPAV), directed by Gardner and funded by GCHQ and EPSRC. The Institute was a collaboration between six universities and comprised six 6 projects over three years:

  • AppGuarden: Resilient application stores, lead by David Aspinall, University of Edinburgh
  • Certified verification of client-side web programs, lead by Philippa Gardner, Imperial College London
  • Se-Ma-Match: Semantic malware matching, lead by Andy King, University of Kent and David Clark, University College London
  • REVES: Reasoning in verification and security, lead by Andrei Voronkov, The University of Manchester
  • Compositional security analysis for binaries, lead by Pasquale Malacaria, Queen Mary University of London, Andy King, University of Kent and Byron Cook, University College London
  • Program verification techniques for understanding security properties of software, lead by Brad Karp, University College London

The projects and investigators covered the breadth of analysis and verification techniques, with expertise in theorem provers, program logics, symbolic verification, information flow analysis, testing, run-time verification, compiler technology and language formalisation. Our skills range from fundamental theory to industrial-strength tools. Our methods have
been used for many programming languages and evaluated on diverse applications.

All the lead investigators from RIAPAV will take part in the new institute, bringing their expertise in fields such as mathematical logic, programming languages, and program analysis and verification.