Funded Proposals

April 2019 – March 2020

The Third call for proposals in October 2018 was on `Verified Trustworthy Software Components’ and proposals were expected to address the problems associated with the aim of placing verified trustworthy software components within the overall software infrastructure.

The call received 35 applications of which 8 were funded. The following projects were selected for funding:

  • Persistent Safety and Security, PI Brijesh Dongol, University of Surrey
  • Reliable High-Level Synthesis, PI John Wickerson, Imperial College London
  • Generalised static checking for type and bounds errors, PI Stephen Kell, University of Kent
  • Higher-order Program Invariants and Higher-order Constrained Horn Clauses, PI Steven Ramsay, University of Bristol
  • Fluid Session Types: End-to-End Verification of Communication Protocols, PI Nobuko Yoshida, Imperial College London
  • Mechanising the theory of build systems, PI James McKinna, University of Edinburgh
  • Formal Verification of Information Flow Security for Relational Databases, PI Andrei Popescu, Middlesex University London
  • Where software meets hardware: Verifying performance impacts of micro-architecture vulnerability mitigations, PI Vashti Galpin, University of Edinburgh

April 2018 – March 2019

The Second call for proposals in October 2017 aimed at supporting work engaging with the international academic or industrial community specialising in analysis, testing and verification, or the UK industrial community interested in applying such techniques to industrial practice. It also encouraged applications for PhD studentships.

The call received 33 applications of which 10 were funded. The following projects were selected for funding:

  • A Foundation for Testing and Verifying C++ Transactions, PI John Wickerson, Imperial College London.
  • Automated black-box verification of networking systems, PI Alexandra Silva, University College London.
  • Building Verified Applications in CakeML, PI, Scott Owens, University of Kent.
  • Formal Verification of Quantum Security Protocols using Coq, PI Raja Nagarajan, Middlesex University London.
  • Generating Exploitable Crashes, PI, John Galea, University of Oxford.
  • Operating system components as verified libraries, PI Tom Ridge, University of Leicester.
  • Session Type-Based Verification Framework for Message-Passing in Go, PI, Nobuko Yoshida, Imperial College London.
  • Specification and verification of C++ data structure libraries, PI Mark Batty, University of Kent.
  • Supervectorizer (phase II), PI Greta Yorsh, Queen Mary University of London.
  • Trustworthy Software for Nuclear Arms Control, PIs Aziem Chawdhary and Andy King, University of Kent.

August 2017 – March 2018

The inaugural call for proposals in June 2017 had a focus on the transfer of technology from academia to industry. It aimed at funding small projects on ambitious blue-sky research as a step towards more standard funding and to provide some continuity funding for projects previously funded by RIAPAV.

The call received over 24 applications of which 8 were funded. You can find details below and in the VeTSS annual report 2017-8.