Showing cs.CRShow all
2 papers · 1 filter
cs.CR2025
Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Stefan Zetzsche, Jean-Baptiste Tristan, Tancrede Lepoint +1
The Fisher-Yates shuffle is a well-known algorithm for shuffling a finite sequence, such that every permutation is equally likely. Despite its simplicity, it is prone to implementa…
cs.CR2024
Verified Foundations for Differential Privacy
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint +7
Differential privacy (DP) has become the gold standard for privacy-preserving data analysis, but implementing it correctly has proven challenging. Prior work has focused on verifyi…