Randomised Testing of the Dafny Compiler: Into the CI
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change
14:00 - 15:30 | |||
14:00 18mTalk | Baking for Dafny: A CakeML Backend for Dafny Dafny Daniel Nezamabadi Chalmers University of Technology and University of Gothenburg, Magnus O. Myreen Chalmers University of Technology | ||
14:18 18mTalk | Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean Dafny Wojciech Różowski University College London, Georges-Axel Jaloyan Amazon Web Services, Sean McLaughlin Amazon Web Services | ||
14:36 18mTalk | Performant, Readable and Interoperable Rust from Dafny Dafny Mikael Mayer Automated Reasoning Group, Amazon Web Services, Shadaj Laddad University of California at Berkeley, Fabio Madge Automated Reasoning Group, Amazon Web Services, Siva Somayyajula Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services | ||
14:54 18mTalk | Randomised Testing of the Dafny Compiler: Into the CI Dafny Karnbongkot Boonriong Imperial College London, Alastair F. Donaldson Imperial College London, Stefan Zetzsche Amazon Web Services | ||
15:12 18mTalk | Teaching Types and Non-Interference in Dafny Dafny Bryan Parno Carnegie Mellon University |