Meeting 70
Host: Michael Butler
Location: Southampton, UK
Dates: 7–11 September 2026
Hotel: Chilworth Manor
Attendees
- Manfred Broy
- Michael Butler
- Sophia Drossopoulou
- Alberto Griggio
- Son Hoang (local observer)
- Peter Höfner
- Cliff Jones
- Rajeev Joshi
- Ben Kaminski (observer)
- Gerwin Klein
- Rustan Leino
- Larissa Meinicke
- Stephan Merz (observer)
- Roland Meyer (observer)
- Mae Milano (observer)
- Toby Murray
- Zoe Paraskevopoulou (observer)
- Clément Pit-Claudel (observer)
- Reza Rezazadeh (local observer)
- Kostis Sagonas (observer)
- Asieh Salehi Fathabadi (local observer)
- Shankar
- Viktor Vafeiadis (observer)
- Pamela Zave
Sessions
Monday September 7
-
All attendees, roundtable introduction
-
Stephan Merz, Understanding Raft
-
Clement Pit-Claudel, Verified compiler bootstrapping
-
Tony Hoare Memorial – livestream in meeting room
Tuesday September 8
-
Manfred Broy, Time after time: fair merge
-
Zoe Paraskevopoulou, Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens
-
Toby Murray, Verified Certified Robustness for Neural Networks
-
Roland Meyer, Program logics for reasoning about concurrent programs under weak consistency
-
Viktor Vafeiadis, Release-guarantee reasoning under weak memory consistency
-
Mae Milano, Verifying the ‘latent spec:’ adventures in Rust interface with C and inline assembly
Wednesday September 9
-
Benjamin Kaminski, A quantitative intermediate verification language
-
Kostis Sagonas, Optimal Dynamic Partial Order Reduction
-
Pamela Zave, Compositional Network Architecture: Formal semantics
-
Alberto Griggio, Verification of Configurable SRA Systems
Thursday September 10
-
Members’ Meeting
-
Larissa Meinicke
-
Rajeev Joshi, Computation Calculus
-
Rustan Leino, Rethinking the verification pipeline
-
Peter Hofner
Friday September 11
-
Son Hoang, Probabilistic generalised substitution language for probabilistic Event-B
-
Michael Butler, Abstraction and refinement of continuous behaviour in cyber-physical systems
-
Shankar, round table on the impact of LLMs