Verifying the Fisher-Yates Shuffle Algorithm in Dafny
summary
Verified Fisher‑Yates implementation in Dafny defines a functional model on bitstreams, proves it yields each permutation with probability 1/n! for duplicate‑free inputs, then gives an executable array method and a formal equivalence proof to imperative array implementation using loop invariants. Proof relies on an abstract probability space and an assumed uniform sampler (compiled to int32/JVM ints); artifacts and proofs are available in the workshop repo and compile to multiple target languages.
AI-written summary · about
chapters (7)
- 0:00Fisher-Yates Shuffle intro
- 2:32Randomness in Dafny
- 5:03Functional Fisher-Yates
- 10:00Correctness proof
- 13:12Imperative implementation
- 14:56Assumptions and summary
- 16:23Q&A
related talks
14mEmbedding Quantum Program Verification into Dafny
21mVerified VCG and Verified Compiler for Dafny
03mAttempts to design hardware using dafny
01h 02mLanguage Design meets Verifying Compilers
26mMechanical Proofs in an Array-Combinator Language
22mRoulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic(…)
22mRandom Variate Generation with Formal Guarantees
05mOn Iteration in Discrete Probabilistic Programming