Testing Specifications in Dafny - Dafny'24
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 17-minute conference talk from ACM SIGPLAN on testing specifications in Dafny. Delve into the challenges of ensuring the correctness of formal specifications in verified systems. Learn about IronSpec, a framework that introduces automatic specification mutation testing and a unit testing methodology for writing Spec-Testing Proofs (STPs). Discover how this approach helps increase trust in specification correctness by flagging discrepancies between original specifications and test writer intent. Examine the evaluation of IronSpec on nine specifications, including three from open-source verified systems, and its effectiveness in uncovering specification bugs. Gain insights into the compromised approach of testing specifications to enhance the reliability of formally verified systems.
Syllabus
[Dafny'24] Testing Specifications In Dafny
Taught by
ACM SIGPLAN
Related Courses
SPARK 2014AdaCore via Independent Automated Reasoning: Symbolic Model Checking
EIT Digital via Coursera Software Testing and Verification
University System of Maryland via edX Haskell for Imperative Programmers
YouTube Model Checking and Temporal Logic - E. Allen Emerson's Turing Award Lecture
Association for Computing Machinery (ACM) via YouTube