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:
- Neural Network Verification: in Search of the Missing Spec, PI is Ekaterina Komendantskaya, Heriot-Watt University
- Type-driven data-science infrastructure for Idris2, PI is Ohad Kammar, University of Edinburgh
- Symbolic Computation for Mainstream Verification, PI is Budi Arief, University of Kent
- Verified Program Synthesis for Refactoring Rust Programs, PI is Meng Wang, University of Bristol
- Safe and Reliable Concurrent Robotics Programming with Choreographies, PI is Nobuko Yoshida, Imperial College London
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.
- 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