Automated Verification of the Parallel Bellman--Ford Algorithm

on YouTube ↗15m

" summary

First deductive verification of an unoptimized GPU Bellman–Ford: mechanized proof shows data-race freedom plus soundness and completeness of shortest distances by encoding three loop invariants and several lemmas, using an atomic min for relaxations and a permission-based graph encoding. Verification runs through VerCors/Viper/Z3, required heavy annotations and small guiding assertions, and completes in six weeks and 12 minutes of total effort, producing a working formal proof that scales to optimized variants.

AI-written summary · about

" chapters (15)

1. 0:00Introduction
2. 0:10Overview
3. 1:00Outline
4. 1:22Input
5. 1:42Algorithm
6. 3:40Post Conditions
7. 4:14Invariants
8. 4:35Simple Path
9. 5:00Simple Path Proof
10. 9:33Verification Tools
11. 10:12Algorithm Overview
12. 11:00Graphs
13. 11:17Permissions
14. 12:47Contradictions
15. 14:39Future work