One of the main aims of VeTSS is to support the UK verification community, and to this end we have funded research projects on analysis, testing and verification, both via small grants and funding calls aligned with VeTSS research. All projects funded so far are below, and you can find details of our upcoming calls  for proposals here.  

2023

Three projects were funded via the Research aligned with cybersecurity research funding call, worth £7.5M open to research projects aligned with the four EPSRC-National Cyber Security Centre (NCSC) research institutes.

• Narges Khakpour (Newcastle University), Sven Schewe (University of Liverpool) and Dominik Wojtczak (University of Liverpool) received funding for their project TRUSTED: SecuriTy SummaRies for SecUre SofTwarE Development with industry partners Google and OCamlPro.
• Jeremy Singer (University of Glasgow), Alice Miller (University of Glasgow) and Zheng Wang (University of Leeds) were funded for their project M4Secure: Making Memory Management More Secure with industry partners Meta (Previously Facebook) and Microsoft.
• Brijesh Dongol (University of Surrey), Gregory Chockler (University of Surrey) and Azalea Raad (Imperial College London) with their project SACRED-MA: Safe And seCure REmote Direct Memory Access with industry partners ARM and nVIDIA, as well as academic partners Cornell University, Max Planck Institutes, Tel Aviv University, and University of Colorado at Boulder.

From 2019 to 2021 VeTSS funded 38 projects via small grants, supporting 46 academics and 10 PhD scholarships at 18 universities across the UK, and awarding a total of £2.5 M.

2021

• Safe and Reliable Concurrent Robotics Programming with Choreographies, PI: Nobuko Yoshida, Imperial College London.
• Verified Program Synthesis for Refactoring Rust Programs, PI: Meng Wang, Co-I: Cristina David, University of Bristol.
• Symbolic Computation for Mainstream Verification, PI: Budi Arief, Co-I: Tom Seed, University of Kent
• Type-driven data-science infrastructure for Idris2, PI: Ohad Kammar, University of Edinburgh.
• Neural Network Verification: in Search of the Missing Spec, PI: Ekaterina Komendantskaya, Co-I: Guy Katz  and  Javier Diaz, Heriot-Watt University

2020

• CONVENER: Continuous Verification of Neural Networks. PI: Ekaterina Komendantskaya, Heriot-Watt University, Co-I: David Aspinall, University of Edinburgh
• Quantitative Algebraic Reasoning for Hybrid Programs: reasoning precisely about imprecisions. PI: Alexandra Silva, Co-Is: Fredrik Dahlqvist and Renato Neves, University College London
• Validating the Foundations of Verified Persistent Programming. PI: Azalea Raad, Co-I: John Wickerson, Imperial College London
• Aion: Verification of Critical Components’ Timely Behavior in Probabilistic Environments. PI: Vincent Rahli, Co-I: David Parker, University of Birmingham
• Mechanising Concurrent WebAssembly. PI: Neel Krishnaswami, Co-Is: Conrad Watt and Jean Pichon, University of Cambridge
• Fixing the thin-air problem: ISO dissemination. PI: Mark Batty, Co-I: Simon Cooksey, University of Kent

2019

• Where Software Meets Hardware: Verifying Performance Impacts of Micro-Architecture Vulnerability Mitigations. PI: Vashti Galpin, Co-I: David Aspinall, University of Edinburgh
• Formal Verification of Information Flow Security for Relational Databases. PI: Andrei Popescu, University of Sheffield,  Co-I: Peter Lammich, University of Twente, The Netherlands.
• Mechanising the Theory of Build Systems. PI: James McKinna, Co-I: Perdita Stevens, University of Edinburgh.
• Fluid Session Types: End-to-End Verification of Communication Protocols. PI: Nobuko Yoshida, Imperial College London, Co-I: Rumyana Neykova, Brunel University London.
• Higher-order Program Invariants and Higher-order Constrained Horn Clauses. PI: Steven Ramsay, University of Bristol, Co-I: Luke Ong, University of Oxford.
• Generalised static checking for type and bounds errors. PI: Stephen Kell, University of Kent.
• Reliable High-Level Synthesis. PI: John Wickerson, Imperial College London
• Persistent Safety and Security. PI: Brijesh Dongol, Co-I: Francois Dupressoir, Co-I, John Derrick, University of Sheffield

2018

• Session Type-Based Verification Framework for Message-Passing in Go. PI: Nobuko Yoshida, Imperial College London
• Automated Black-Box Verification of Networking Systems. PI: Alexandra Silva, University College London, Co-I: Matteo Sammartino, Royal Holloway, University of London
• Specification and verification of C++ data structure libraries. PI: Mark Batty, University of Kent.
• Towards Optimised Taint Analysis. PI: Daniel Kroening, University of Oxford, Amazon, Co-I: John Galea, University of Oxford
• Building Verified Applications in CakeML . PIs: Olaf Chitil and Scott Owens, University of Kent.
• Trustworthy Software for Nuclear Arms Control. PI: Andy King, University of Kent
• Supervectorizer (Phase II). PI:Greta Yorsh, Queen Mary, University of London, 
• Operating Systems Components as Verified Libraries. PI: Tom Ridge, University of Leicester
• Formal Verification of Quantum Security Protocols using Coq. PI: Rajagopal Nagarajan, Middlesex University London.
• A Foundation for Testing and Verifying C++ Transactions. PI: John Wickerson, Imperial College London.