Talk on Slicing at Dafny 2026
· One min read
Darion Haase presented our work on slicing-based diagnostics for probabilistic program verification at Dafny 2026, which took place on January 11, 2026, in Rennes, France.
The presentation gave an overview of the main ideas behind our ESOP 2026 paper "Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing". It gave an introduction to our three notions of slicing (error-witnessing, verification-witnessing, and verification-preserving slices) and explained how they can be used to provide useful and formally justified diagnostics for deductive verifiers like Caesar and Dafny.