Meeting 69
Host: Sophia Drossopoulou
Location: Athens, Greece
Dates: 19–23 May 2025
Talks
Monday 19 May
- All attendees, roundtable introduction
- Peter Müller, Hyper Hoare Logic
- Brijesh Dongol, Correctly Programming Remote Direct Memory Access
- Oded Padon, Duality and primal-dual algorithms in program verification
- Justin Hsu, Type Systems for Numerical Error Analysis
- Benjamin Kaminski, Iteration Logic - a logic for reasoning about fixed points of endomaps on complete lattices
Tuesday 20 May
- Rustan Leino, Reasoning about allocation
- Alberto Griggio, Information exchange for software verification
- Clement Pit-Claudel, Modern regular expressions, with a focus on semantics and matching complexity
- Mae Milano, Gambit: sequential consistency without coordination in distributed programming languages
- Ori Lahav, Hyperproperty-Preserving Register Specifications
- Roderick Bloem, Learning a Mealy machine from a language
- Viktor Vafeiadis, Automatically establishing correctness of concurrent libraries
Wednesday 21 May
- Cliff Jones, Rely-Guarantee ‘thinking’ for Real-Time Scheduling
- Zoe Paraskevopoulou, Correctness for the Ground Up for Ethereum Smart Contracts
- Alex Summers, Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing System
- Roland Meyer, Verification under Weak Consistency and Recent Decidability Results in Verification
Thursday 22 May
- Mark Santolucito
- Stephan Merz, TLA+ Proof System
- Members’ Meeting
- Gerwin Klein, The next 700 verified kernels
- Sophia Drossopoulou
- Thomas Wies, Characterizing Implementability of Global Protocol Specifications
Friday 23 May
- Sophia Drossopoulou, Holistic Specifications and Reasoning about External Calls
- Yannis Smaragdakis, Program Analysis for High-Value Smart Contract Vulnerabilities
- Kostis Sagonas, Optimal Algorithms for Stateless Model Checking
- Gerwin Klein
- Grace Dinh
- Rajeev Joshi, Checking Concurrent Production Code