Tutorial at VeTSS Summer School 2026

Created in July 07, 2026

2026

I will be giving a tutorial together with Achim Brucker at the VeTSS Summer School 2026, taking place at the University of Exeter from 3–6 August 2026.

Our tutorial, https://vetss.org.uk/vss-26-programme/, provides a practical introduction to interactive theorem proving with Isabelle/HOL. We will discuss Isabelle’s LCF-style foundation, its proof automation capabilities, and show how Isabelle can be used not only for verification but also as a platform for developing custom formal methods tools.

The tutorial is designed as a hands-on experience, combining short theoretical presentations with guided laboratory exercises. Participants will also get an introduction to Isabelle/ML and learn how to extend Isabelle for domain-specific applications.

The VeTSS Summer School is a graduate school focused on program analysis, testing, and verification, bringing together PhD students and early-career researchers from across the UK and beyond.