Funded Projects

April 2021 – March 2022

The Fifth Annual VeTSS Call for Proposals: Safe and Secure Software Systems was the last VeTSS call associated with the current funding from EPSRC and NCSC. The call for proposals, under the theme: ‘Safe and Secure Software Systems’, addressed new work loosely grouped under the headings Safe AI, Trustworthy Software, Verified Software Infrastructure and Reliable Continuous Software Behaviour. The call received 20 applications from researchers and institutions across the UK, of which the following were selected for funding:

April 2020 – March 2021

The Fourth call for proposals in October 2019, ‘Digital Security through Verification’ focussed on how to embed verification into the heart of our modern software systems. The call complemented the ISCF ‘Digital Security by Design’ programme, which had the specific focus on capability hardware, building on a proposed Arm processor and the work of the CHERI project at the University of Cambridge.

The call received 24 applications of which 6 were funded. The following projects were selected for funding:

  • Fixing the thin-air problem: ISO dissemination, PI Mark Batty, University of Kent
  • Mechanising Concurrent WebAssembly, PI Neel Krishnaswami, University of Cambridge
  • Aion: Verification of Critical Components’ Timely Behavior in Probabilistic Environment, PI Vincent Rahli, University of Birmingham
  • Validating the Foundations of Verified Persistent Programming, PIs Azalea Raad and John Wickerson, Imperial College London
  • Quantitative Algebraic Reasoning for Hybrid Programs: reasoning precisely about imprecisions, PI Alexandra Silva, University College London
  • CONVENER: Continuous Verification of Neural Networks, PI Ekaterina Komendantskaya, Heriot-Watt University

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 projects were below selected for funding and you can find full details of each project on the VeTSS annual report 2018-9.

  • 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.