Thanks to funding from the National Cyber Security Centre, VeTSS funds research projects on analysis, testing and verification, both via small grants and funding calls aligned with VeTSS research.
2022
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.
VeTSS has also 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. You can find a list of projects funded via the small grants call below.
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.
2017
- Mechanised Assume-Guarantee Reasoning for Control Law Diagrams via Circus. PI: Jim Woodcock, Co-I: Simon Foster, University of York
- PrideMM web interface. PI: Mark Batty, Co-I: Radu Grigore, University of Kent.
- Verifying Efficient Libraries in CakeML. PI: Scott Owens, University of Kent
- Mechanising the metatheory of SQL with nulls. PI: James Cheney, Co-I: Wilmer Ricciotti, University of Edinburgh.
- Automated Reasoning with Fine-Grained Concurrent Collections. PI: Ilya Sergey, University College London, Co-I Nikos Gorogiannis, Facebook and University of Middlesex.
- EASTEND: Efficient Automatic Security Testing for Dynamic Languages. PI: Johannes Kinder, Royal Holloway, University of London.
- Supervectorizer. PI: Greta Yorsh, Queen Mary, University of London
- Automated Testing for Web Browsers. PI: Benjamin Livshits, Imperial College London, Co-I: Alastair Donaldson, Imperial College London, Google