VeTSS Research Award 2025

Awardees

Six projects were funded via VeTSS Research Award 2025 funding call, worth 250k and open to research projects aligned with VeTSS research on topics including, but not limited to, those outlined in the VeTSS Problem Book. Congratulations to the awardees, especially the proposals led by early career researchers (ECRs) and by researchers currently underrepresented in computer science and / or belonging to marginalised communities. 

  • Unlocking Hardware Verification via Software Algorithm Specifications, PI: Dr Jianyi Cheng, University of Edinburgh, Co-I: Dr Yann Herklotz, EPFL.
  • Probabilistic Precision Tuning, PI: Fredrik Dahlqvist, Queen Mary University of London.
  • Relational Dualities for Program Logics, PI: Alex Kavvos, University of Bristol.
  • Secure Code Generation with Large Language Models, PI: Arindam Sharma, Co-I: Cristina David, University of Bristol.
  • Formalised Software Requirements for Human-Robot Teamwork, PI: Hazel M. Taylor, Co-I: Marie Farrell, University of Manchester.
  • Translation Validation for SuperOptimized Cryptographic Software, PI: François Dupressoir, Co-I: Daniel Page, University of Bristol.

Unlocking Hardware Verification via Software Algorithm Specifications

PI: Dr Jianyi Cheng, University of Edinburgh, Co-I: Dr Yann Herklotz, EPFL

This research proposes rethinking the development flow for hardware development and verification, exploiting existing software verification techniques. We plan to extend Dafny  to hardware verification, a well-known verification language that shares various similar (object-oriented) features with existing HLS languages like C++. Dafny has been shown to work at immense scale, currently being used by Amazon AWS to implement and verify their software authorisation engine, being invoked 1 billion times per second for over a year without an incident in 2024. The outcome of this research is an open-source hardware development tool that enables users to develop their algorithms with verified specifications in Dafny, where the algorithms and their specifications will be translated into high-performance hardware in SystemVerilog and hardware specifications in SystemVerilog Assertions (SVAs) for both deployment and verification.

PI: Dr Jianyi Cheng  University of Edinburgh

PI: Dr Fredrik Dahlqvist  Queen Mary University of London

Probabilistic Precision Tuning

PI: Fredrik Dahlqvist, Queen Mary University of London.

The aim of this project is to upgrade PAF [2, 3], a tool for the Probabilistic Analysis of Floating-point errors co-developed by the PI, into a practical Probabilistic Precision Tuning tool. This is a tool that takes as inputs (i) a numerical routine, (ii) the probability distribution of the routine’s inputs, (iii) a probabilistic post-condition of the shape ‘the roundoff error exceeds a threshold E with probability less than ϵ’, and returns the most economical floating-point format for which this probabilistic post-condition holds. The required improvements to PAF to reach this goal will be based on existing results and prototypes, and we therefore expect significant improvements to PAF at a relatively low cost in terms of research hours. The proposal is structured around two improvements we plan to make to PAF: (1) allowing routines with conditional branching (currently unsupported by PAF), and (2) computing exact polynomial expressions over random variables using Cylindrical Algebraic Decomposition (PAF currently computes complex approximations using an SMT solver). These improvements are interesting and important in their own right and will provide new methods and tools for the understanding of probabilistic programs in general.

Relational Dualities for Program Logics

PI: Dr Alex Kavvos. University of Bristol

This project proposes a blue-skies investigation of a new class of dualities—relational Stone-type dualities—that could reshape the foundations of program logics. We will explore such dualities, aiming to reveal new structural connections between bisimulations, system behaviour and logical reasoning. The resulting theory could lead to new tools for reasoning about program transformations, relational logics, and compiler correctness. The project operates at Verification Technology Readiness Level 1 (VTRL 1) and will be carried out through a 1-year Masters by Research project.

PI: Dr Alex Kavvos    University of Bristol

PI: Arindam Sharma  University of Bristol

Secure Code Generation with Large Language Models

PI: Arindam Sharma, Co-I: Cristina David, University of Bristol.

This project aims to improve the security code generated by large language models by developing constrained decoding algorithms that enforce security policies throughout the generation process—ensuring that all outputs satisfy security constraints before they are presented to the user. In this proposal we will focus on the secure generation of C and C++ code.

Formalised Software Requirements for Human-Robot Teamwork

PI: Hazel M. Taylor, Co-I: Marie Farrell, University of Manchester

Autonomous systems are increasing in complexity and capability. It is becoming clear that Human-Robot teams will be tasked with completing safety- and mission-critical tasks, especially in domains where (embodied) AI interacts with the physical world. Examples include autonomous robotic systems that (1) reduce human exposure to hazardous environments such as in nuclear applications, and (2) enable operations that are simply not possible for humans in isolation due to hazardous and hostile environments such as in-space manufacturing. In these critical settings, humans must work alongside AI-driven robots to complete complex tasks. However, no explicit software requirements exist to enable and verify this interaction. Requirements are central to software development, verification and assurance processes in critical, often highly-regulated, domains so their absence undoubtedly limits the use of Human-Robot teams in critical sectors. This project will fill this gap, removing the barrier to the use of Human-Robot teams through the provision of a taxonomy and suite of formalised software requirements that can be used to ensure that Human-Robot teams demonstrate safe, verifiable teamwork. By providing a structured foundation for designing and verifying Human-Robot collaboration, this work will enable reliable and verifiable integration of AI into diverse, cyber-physical, teams.

 PI: Hazel M. Taylor    University of Manchester

PI: François Dupressoir  University of Bristol

Translation Validation for SuperOptimized Cryptographic Software

PI: François Dupressoir, Co-I: Daniel Page, University of Bristol

We propose to identify and prioritize opportunities for research and innovation for the verification of high-performance cryptographic software. In particular, we focus on exploring the development and use of superoptimization and translation validation tools, enabling fast and safe diversification of hardware targets benefitting from recent advances in high-assurance cryptographic engineering. We aim for those activities to produce: broadly disseminated reports outlining opportunities, and estimating and quantifying their potential impact; as well as small software demonstrators. We include planning of future research and innovation funding in the proposed activities.