Funded Proposals | UK Research Institute in Verified Trustworthy Software Systems

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.