Skip to content
- 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