VeTSS Annual Conference 2025

The VeTSS Annual Conference is a key event for professionals from both academia and industry who are passionate about program analysis, testing, and verification. This open and inclusive gathering offers a unique opportunity to connect, share ideas, and stay at the forefront of cutting-edge research and innovation.

This year’s conference will feature exciting announcements, including the launch of the VeTSS Small Grants Scheme and the presentation of the VeTSS PhD Awards.

Registration is now closed. Please email us at contact@vetss.org.uk if you wish to be added to the waiting list. 

This year’s event will be held at the Royal Academy of Engineering, London on Friday, 6th of June. You can find the address and full directions to the venue on this link.

The meeting with start at 9:00. Registration, with tea and coffee, is from 8:30. On arrival, please make your way up to the ERA Foundation room on the first floor. You will be able to collect your badge there.

Please find the draft programme below. The detailed schedule will be updated periodically.

We want to make every VeTSS event a respectful and friendly environment for all, and we ask that everyone attending the Annual conference adheres to the VeTSS code of conduct.

Programme

Details of talks

In Search of Oracles: Testing Systems that Reason about Code

Alastair Donaldson (Imperial College London)

Abstract:

The world’s deployed software relies on sound program reasoning by compilers that generate low level code. The hardware devices on which this software runs are validated using equivalence checking tools that perform intricate reasoning to confirm that a design correctly implements a high level specification. We use verification tools to gain confidence in critical software components by source code level reasoning. And, increasingly, we rely on large language models to aid in the understanding of software, including to find exploitable vulnerabilities ahead of time. These are all examples of systems that reason about code. How do we go about validating these systems? In this keynote I will provide an overview of recent and ongoing research, with various collaborators, on devising test oracles to automatically find bugs in compilers, equivalence checkers and program analysis tools, and to help map out the reasoning boundary of a given large language model.

Formal methods for AI efficiency and automatic quantization

Andrey Rybalchenko (Microsoft Research)

Abstract:

Large Language Models (LLMs) are rapidly emerging as the dominant workload across AI datacenters and edge devices. Their immense computational demands have triggered a wave of innovation aimed at reducing inference costs. This talk presents a novel approach to automating quantization, a technique that lowers inference cost by replacing high-precision LLM operations with more efficient, lower-precision alternatives. At the core of our method is a formulation of quantization as a program synthesis problem, enabling a principled and scalable solution. By integrating this automated quantization step into the LLM deployment pipeline, we’ve achieved over a 10× increase in velocity for shipping quantized models—dramatically accelerating the path from research to production.

Sociotechnical Futures: sociotechnical security for an age of cyber automation

Lizzie Coles-Kemp (Royal Holloway, University of London)

Abstract:

For many sociotechnical cyber security is about usable authentication, frictionless secure interactions, and security built in from the ground-up. The era of cyber automation brings with it the promise of shifting the burden of secure human computer interaction from the end user down through the stack and into the fundamental design of digital technologies and products. Whilst such a shift would certainly be welcome, it raises more sociotechnical questions than it answers and to be effective needs to draw on a wider body of sociotechnical research. Sociotechnical cyber security is founded on questions of secure human computer interaction, but those questions are grounded in far more fundamental questions of security. Consequently, over the last 10 years sociotechnical cyber security has evolved to include fundamental questions that focus on how to design for inclusive security, that critically challenge notions of who benefits from cyber security, and that explore how cyber security shapes and is shaped by a wider set of securities. The era of cyber automation brings such fundamental questions to the fore and concretely impacts how we design trustworthy software systems. In this talk I shall sketch out some of these concrete impacts and set out a call to action for an interwoven research agenda that underscores the importance of a co-design that spans the disciplines represented by the UK’s cyber security research institutes. Such a research agenda has the potential to positively shape an age of cyber automation.

Formal is Fast — Optimizing and Verifying ML-KEM

Hanno Becker (AWS)

Abstract:

This talk presents mlkem-native, a C/Assembly implementation of the ML-KEM post-quantum cryptography standard. mlkem-native is fast through selected use of (super-)optimized assembly, and trustworthy through extensive formal verification: All C code is proved memory-safe and type-safe using CBMC, and all AArch64 assembly is proved functionally correct using HOL-Light. The result is an implementation that is not only fast, but fast to deploy: Formal verification allows for the confident adoption of complex code that would otherwise be difficult to gain trust in.

Modelling and Verification of Quantum Systems

Rajagopal Nagarajan (QUƎNT∀NGLE)

Abstract:

Compositional automata learning for evolving systems

Mohammad Mousavi (King’s College London)

Abstract:

Model learning is a technique to learn behavioural models by interacting with black-box systems. Variability and evolution are inherent to much of the modern systems and hence, new sorts of model learning techniques are needed to learn about variability-intensive and evolving systems. Moreover, model learning faces challenges when dealing with large scale systems. Compositional learning addresses the scalability issue by parallelising the learning process into learning the behaviour of system components. In this talk, we first present the basic principles of automata learning and then report on novel techniques for learning variability-aware models as well as efficient learning for evolving systems by identifying the commonalities and differences in the learning process. We conclude with some of our recent results on compositional automata learning.

Reflections on Property Based Testing

Samantha Frohlich (University of Bristol)

Abstract:

Property-based testing (PBT) allows for more thorough testing by checking programs against properties that are tested using randomly generated values. However, specifying both properties and random generators for creating these random values is non-trivial. Expert users of property-based testing often labour to craft random generators that encode detailed knowledge about what it means for a test input to be valid and interesting. To address this, I will present “Reflective Generators”, which allow users to get more out of their generators once they have been defined. I will then advocate that more needs to be done, and that this is actually something I need help with. Increasing returns for user effort was a step in the right direction, but this is a “Programming Languages” (PL) solution. To address the root problem, that PBT is hard for users, we need a “Human-Computer Interaction” (HCI) solution. I end by advocating that learning from and working with this community will be vital in the future of testing, verification, and security.

Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice

Mark Batty (University of Kent)

Abstract:

We present a thin-air-free weak memory model that admits compiler optimisations that aggressively leverage knowledge from alias analysis, an assumption of freedom from unde!ned behaviour, and from the extrinsic choices of real implementations such as over-alignment. Our model has tooling support with state-of-the-art performance, executing a battery of tests quicker than other executable thin-air free semantics. The model integrates with the C/C++ memory model through an exportable semantic dependency relation, it allows standard compilation mappings for atomics, and it matches all tests in the recently published desiderata for C/C++ from the ISO.