Randomised Testing of the Dafny Compiler: Into the CI
summary
Integrates the fuzzer fuzz-d into Dafny’s CI as CompFuzzCI, running a brief per‑PR fuzzing campaign in containers, auto‑reducing and attempting bisection, and reporting failures as PR comments or GitHub issues. Deployment finds three previously unknown bugs in one month; a retrospective simulation over 20 historical bugs shows 6/20 always found, 14 never found. CI fuzzing catches many edge cases quickly but needs longer nightly runs and better handling of unsupported features and historical build differences.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:40Fuzzer detects compiler bugs
- 3:27Fuzzing critical for Dafny
- 4:31Manual steps in fuzzing
- 5:36Problem with manual fuzzing
- 6:39Automating fuzzing in CI
- 7:44Unsupported features challenges
- 9:53Start fuzzing compiler
- 10:14Automating bug bisection
- 12:44CI-friendly changes for bisection
- 13:05Simulating CI fuzzing effectiveness
- 14:50CI fuzzing versus nightly runs
- 15:11Key takeaways and future
- 15:54Q&A
