VeTSS Summer School 2026 Programme
Details of talks
An introduction to the Tile IR memory model
Simon Cooksey (NVIDIA)
Abstract:
The GPU is a highly concurrent system, with thousands of threads operating on shared memory to contribute each part of a solution to a hilariously parallel problem. The NVIDIA GPU memory model is given for the PTX virtual ISA, which provides a C++-like abstraction of the hardware threads. That C++-like nature means a lot of the constraints of C++ are imposed on the memory model and programming model as a whole. The GPU has also incorporated new accelerators which massively improve performance for common tensor operations, as well as accelerators for address calculation and data movement. These accelerators behave increasingly in a non-C++ way, so the programming model must adapt.
This motivates languages like OpenAI’s Triton and NVIDIA’s Tile IR. These are languages which dispense with normal per-element computation as you would write in other programming languages, and instead have whole block-of-threads control flow. With the difference in programming model comes a difference in memory model, and while the changes are small, the power for both compiler and hardware optimisation is profound.
In this session I will explain how axiomatic memory models are forumulated, going from a simple model of sequential consistency to the Tile IR memory model with it’s “token ordering”. The first 45 minutes will cover typical axiomatic models, and the second 45 minutes will go over Tile IR in depth, and demonstrate why the differences between the Tile IR memory model facilitates optimisations which are either impossible or extremely cumbersome in a more traditional programming language/memory model combination.
From Foundations to Tool Building: A Hands-On Introduction to Isabelle/HOL and Isabelle/ML
Achim Brucker and Diego Marmsoler (University of Exeter)
Abstract:
Interactive theorem provers, such as Isabelle/HOL, have proven to be powerful platforms for industrial-grade software verification, security analysis, and domain-specific engineering. This tutorial provides a practical introduction to Isabelle/HOL, highlighting its unique combination of high trustworthiness and a high degree of automation. Its trustworthiness is rooted in an LCF-style small trusted core, guaranteeing that every proof is strictly checked from foundational first principles. Simultaneously, Isabelle drastically reduces manual verification effort through advanced automation, prominently featured by tools like Sledgehammer.
Moving beyond standard verification, we will demonstrate that Isabelle is much more than just a theorem prover: it is a versatile platform for building custom formal methods tools. By lifting the hood to introduce Isabelle/ML, participants will learn how to extend the prover’s capabilities for their own domain-specific applications.
The tutorial is designed as a highly interactive “hands-on” experience, seamlessly interleaving theory with guided lab sessions. Participants should have Isabelle installed prior to the start of the tutorial (detailed instructions will be sent out before the tutorial).
Formal Language Semantics and Program Verification in Lean
Wojciech Różowski (Lean FRO)
Abstract:
Lean is a functional programming language that doubles as an interactive theorem prover, allowing one to write programs and reason about their correctness within a single tool. In this course, students will learn how to use Lean to deeply embed a prototype imperative programming language (Imp), design custom surface syntax using Lean’s macro system, and implement a monadic interpreter. The course will then focus on how to write formal proofs about the language and its interpreter using Lean tactics.
The code that will accompany this tutorial can be found at: https://github.com/wkrozowski/vetss2026. Please follow the instructions to prepare for the Tutorial.
Counter machines and the border of effective computation
Patrick Totzke (University of Liverpool)
Abstract:
Counter Machines a la Minsky are one of the simplest computational models and a great starting point to explore the limits of effective computability and verification.
We will recall some foundational results in the theory of computation, including the undecidability of the termination problem for two-counter machines and related decision questions. These provide natural starting points to show impossibility results and complexity lower bounds.
We will survey ways to modify the model to make it less expressive and allow to recover decidability for verification questions.
This can be achieved by restricting the use of zero-tests, accepting imprecise updates to counters, allowing a single counter, or combinations thereof.
Several such models form the theoretical underpinning of automated formal verification methods in use today and we will demonstrate applications and directions for future research.
Formal Methods for Safe Reinforcement Learning
Edwin Hamel-De le Court (University of Manchester)
Abstract:
The goal of the lecture is to present the emerging relationship between Reinforcement Learning (RL) and Temporal Logic (TL). The topic is an active area of research that builds a bridge between the RL and verification communities. In a world where the safety of AI systems is becoming increasingly critical, bridging the gap between these communities is an important step towards developing safe, reliable, and trustworthy AI.
At the end of the lecture, the audience will have the basics of RL and safe RL, a good intuition of the properties expressible in Temporal Logic, and a clear overview of how to design RL algorithms with TL objectives or constraints, including methods that provide formal guarantees.
Analysis of EMV payment security, the case for curiosity driven cyber security research
Tom Chothia, (University of Birmingham)
Abstract:
In this session I will make the case for curiosity driven cyber security research based on human understanding of complex systems, and I will show how formal modelling can support this. This is in contrast to AI-based methods or tool-based methods, such as fuzzing, which focus on results without building deeper understanding. I’ll give an examples of this from my recent work on verification of EMV payment systems .
The EMV contactless bank card payment system has many independent parties who have unilaterally added undocumented features to the core protocol specifications. Our research has shown that formal verification is an effective method to understand, explain and test the security of EMV. Highlights of our work include taking $10,000 from the locked iPhone of YouTube influencer MKBHD and enabling an offline Square reader to accept transactions from fake cards for £20,000. In addition to finding vulnerabilities, we have designed a security protocol for smart cards (currently being added to the ISO 14443 standard) and used formal verification to show that it stops most attacks against EMV.
This case study shows that an effective way to do cyber security research is to be driven by your own curiosity to build a human understanding of complex systems, and that while computers now govern most aspects of our lives, it is still occasionally possible for us to outwit these systems and beat the machines.
by