YoVDO

Dafny Test Generation - Automated Testing for Verified Programs

Offered By: ACM SIGPLAN via YouTube

Tags

Automated testing Courses Chess Courses Formal Methods Courses Dafny Courses

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
Explore the latest advancements in automated testing for Dafny programs through this 17-minute conference talk presented at ACM SIGPLAN. Delve into the capabilities of DTest, a toolkit designed to enhance confidence in Dafny code execution. Learn how DTest enables runtime verification of proven properties and facilitates comparison with existing reference implementations. Witness a live demonstration using an illustrative Dafny program that formalizes chess rules, showcasing DTest's ability to generate targeted test cases for complex scenarios. Discover how DTest leverages the Dafny verifier to efficiently select specific chess positions, outperforming traditional fuzzing techniques in certain contexts. Examine the newly introduced coverage report feature, which identifies provably unreachable code segments. Gain insights into how DTest's system-level test generation and dead code identification can help developers uncover conflicting specifications and potential implementation bugs in their Dafny projects.

Syllabus

[Dafny'24] Dafny Test Generation


Taught by

ACM SIGPLAN

Related Courses

Teaching Logic and Set Theory with Dafny
ACM SIGPLAN via YouTube
CLOVER: Closed-Loop Verifiable Code Generation - Dafny'24
ACM SIGPLAN via YouTube
Verifying a Concurrent File System with Sequential Reasoning
ACM SIGPLAN via YouTube
Generating Conforming Programs with Xsmith
ACM SIGPLAN via YouTube
Domesticating Automation for Large-Scale Verification Systems - Dafny'24
ACM SIGPLAN via YouTube