POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Sun 19 Jan 2025 14:54 - 15:12 at Room 2 - Backends and Teaching

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 Jan

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:30
Backends and TeachingDafny at Room 2
14:00
18m
Talk
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
18m
Talk
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
18m
Talk
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
18m
Talk
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
18m
Talk
Teaching Types and Non-Interference in Dafny
Dafny
Bryan Parno Carnegie Mellon University