Dafny is a verification-ready programming language that is executed via compilation to C# and other mainstream languages. Recent work has introduced DTest, a toolkit for automated testing of Dafny programs. DTest allows Dafny users to ensure the verified properties hold at runtime once they link the binary against external libraries, or to compare their code to an existing reference implementation. This increases confidence that what is proven in Dafny matches what ultimately gets executed. In one of the prior case studies, DTest was able to successfully perform unit-testing of AWS Encryption SDK (ESDK), one of the largest open-source Dafny projects. In this talk, we are going to showcase the most recent version of DTest and demo its capabilities on an illustrative Dafny example program.

As our example, we will use a Dafny program that formalizes a small subset of the rules for the game of chess. DTest relies on the verifier to pick, from the millions of possible chess positions, those that involve specific kinds of checks and checkmates. This setting puts DTest in contrast with popular fuzzing techniques that can fall short in scenarios like this when simple enumeration of all possible inputs might not be feasible. To emphasize this point, we showcase one of the newest additions to DTest, an automatically produced coverage report that highlights lines of dead code that are provably unreachable regardless of the arrangement of chess pieces provided as input. Dead code identification, along with DTest’s ability to generate system-level tests that use a single method as an entry point, can help developers identify conflicting specifications and potential implementation bugs.