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.
- Mechanising the Metatheory of SQL with Nulls, James Cheney (PI) and Wilmer Ricciotti, University of Edinburgh.
- Verifying Efficient Libraries in CakeML, PI Scott Owens, University of Kent.
- PrideMM web interface, Mark Batty (PI) and Radu Grigore, University of Kent.
- Mechanised Assume-Guarantee Reasoning for Control Law Diagrams via Circus, Jim Woodcock (PI) and Simon Foster, University of York.
- Automated Testing for Web Browsers, Benjamin Livshits (PI) and Alastair Donaldson, Imperial College London.
- Supervectorizer, PI Greta Yorsh, Queen Mary University of London.
- EASTEND: Efficient Automatic Security Testing for Dynamic Languages, PI Johannes Kinder Royal Holloway, University of London.
- Automated Reasoning with Fine-Grained Concurrent Collections, Ilya Sergey (PI), University College London and Nikos Gorogiannis, Middlesex University London