5th-8th August 2025, Manigod, France
A printable version of the program is available here.
“RustyKeY: Deductive Verification of Rust with Dynamic Logic” – Daniel Drodt (long)
“Dynamic Logic à la Locale” – Samuel Teuber (long)
“On Formal Verification with Trace Formulas” – Niklas Heidler (long)
“Kukicha – Efficient Yet Powerful Refinement Types” – Florian Lanzinger (long)
“Interoperable Specification and Verification of Encapsulated Data Structures” – Wolfram Pfeifer (long)
“Confidentiality Check with Deductive Verification” – Asmae Heydari Tabar (short)
“The EU Product Liability Directive” – Richard Bubel (short)
“Formal Verification of Legal Contracts: A Translation-based Approach” – Adele Veschetti (short)
“Towards an Axiomitisation of Solidity Storage and Memory” – Guilherme Silva (short)
“Using Sorting Networks to Assist the Formal Proof” – Thomas Baar (long)
“Multi-Sets in KeY” – Lukas Grätz (short)
“Non-Null Sorts in KeY” – Lukas Grätz (short)
“Equivalent Mutants: Deductive Verification to the Rescue” – Reiner Hähnle (long)
“Extracting Go Code from your Isabelle theories” – Terru Stübinger (long)
“Planning Inter-Model Consistency Recovery” – Henriette Färber (short)
“Timed Contract Automata” – Andreas Bremer (short)
“Synthesis of Auxiliary Specification via Large Language Models” – Nils Buchholz (short)
“Verifying Event Sequences in Correct-by-Construction Programs” – Fynn Demmler (long)
“Scaling Correctness-by-Construction” – Tabea Bordis (long)