Randomised Testing of the Dafny Compiler
summary
Built two generators, fuzz-d (differential testing) and DafnyFuzz (metamorphic testing), plus comparison with XDsmith, and apply reconditioning and value-tracking to produce valid, executable Dafny programs. The tools report about 30 distinct compiler bugs across backends, including multiple soundness failures; nine of the reported bugs are already fixed. fuzz-d produces complementary line/branch coverage versus XDsmith and the regression suite, and mutation testing shows the fuzzers kill many more mutants than existing tests.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:05Test oracle problem
- 2:28Fuzd and DaphneFuzz
- 3:31Program generation approach
- 4:58Differential and metamorphic testing
- 6:41Bug findings and evaluation
- 7:43Coverage vs mutation testing
- 9:07Bug examples in Dafny
- 12:23Live demo
- 14:28Conclusion and Q&A
related talks
20mRandomised Testing of the Dafny Compiler: Into the CI
52mStructure aware fuzzing
26mDifferential Testing with Foundry
38mTesting with two failure seeking missiles: fuzzing and property based testing
53mThree Colours of Fuzzing: Reflections and Open Challenges
18mOptimization-Directed Compiler Fuzzing for Continuous Translation Validation
53mFuzz Testing for Fun and Profit
20mWhat's the fuzz all about? Randomized data generation for robust unit testing