Title: Randomised Testing of the Dafny Compiler: Into the CI
Authors: Karnbongkot Boonriong, Alastair F. Donaldson, Stefan Zetzsche
Conference: POPL 2025

Abstract:
Recently, a new fuzzer, fuzz-d, for testing the Dafny compiler was presented. As is common for compiler fuzzers, it was used in a comprehensive periodic fuzz testing campaign that is decoupled from the development process of the compiler. In this paper, we explore the idea of instead integrating fuzz-d deeply into the development process, by running a brief fuzzing campaign as part of the continuous integration (CI) workflow of each pull request to Dafny’s compiler project. More specifically, we present CompFuzzCI, a framework that seamlessly integrates fuzz-d into Dafny’s compiler CI pipeline. As a byproduct of deploying CompFuzzCI, we discovered three previously unknown bugs. We share the lessons learned from deploying CompFuzzCI and highlight the challenges and successes we encountered. Additionally, we report on a controlled simulation that evaluates whether CompFuzzCI would have been beneficial in identifying bugs in past development cycles. Our findings demonstrate the significant advantages of integrating continuous fuzzing into the CI process, providing valuable insights for other compiler development teams aiming to enhance their bug detection capabilities.

Source: https://popl25.sigplan.org/details/dafny-2025-papers/4/Randomised-Testing-of-the-Dafny-Compiler-Into-the-CI
