Runtime Tests for Dafny

Abstract

Quals talk:

Dafny is a verification-aware programming language that can automatically prove that the implementation of a particular method satisfies its specification. Dafny provides compilers for generating executable code in different target languages, such as C# or Java. A target-language executable generated from Dafny source must, in theory, exhibit the runtime behavior proven by Dafny verifier. In practice, however, compiler bugs and incorrect specification of external methods can lead to the executable producing a result that is different from the one expected. To help ensure that the verified behavior carries over to the target language, I introduce automatically generated runtime tests to Dafny. Automated test generation, which is now officially a part of the Dafny language, is a multi stage process that relies on counterexample extraction and a custom mocking framework. In my talk, I will describe the challenges of generating runtime tests for Dafny and discuss my ideas for extending the existing testing functionality.

Please join meeting in Cummings #402 or via Zoom.

Join Zoom meeting: https://tufts.zoom.us/j/94296243737

Password: see colloquium email

Dial-in not an option for this event.