Thanks to funding from the National Cyber Security Centre, VeTSS is able to fund research projects on analysis, testing and verification. The aim is to support research projects seeking to develop fundamental theories and industrial-strength tools that target real-world applications, and, in particular, research work that can more difficult to fund through, for example, UKRI and industry.

VeTSS Annual Report 2020/2021

Over the last five years,  VeTSS has funded 38 projects, supporting 46 academics and 10 PhD scholarships at 18 universities across the UK, and awarding a total of £2.5 M. Our projects, in chronological order from the latest call, are listed below:

Foreword

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