The third call for proposals 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
The second call for proposals 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.
The inaugural call for proposals received over 24 applications of which 8 were funded. The following projects were selected for funding:
- Mechanising the Metatheory of SQL with Nulls, PI Wilmer Ricciotti, University of Edinburgh.
- Verifying Efficient Libraries in CakeML, PI Scott Owens, University of Kent.
- PrideMM web interface, PI Mark Batty, University of Kent.
- Mechanised Assume-Guarantee Reasoning for Control Law Diagrams via Circus, PI Jim Woodcock, University of York.
- Automated Testing for Web Browsers, PI Benjamin Livshits, Imperial College London.
- Supervectorizer, PI Greta Yorsh, Queen Mary University of London.
- EASTEND: Efficient Automatic Security Testing for Dynamic Languages, PI Dr Johannes Kinder Royal Holloway, University of London.
- Automated Reasoning with Fine-Grained Concurrent Collections, PI Dr Ilya Sergey, University College London.