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
Human Computer InteractionIndependent Introduction à la logique informatique - Partie 2 : calcul des prédicats
Université Paris-Saclay via France Université Numerique System Validation (4): Modelling Software, Protocols, and other behaviour
EIT Digital via Coursera Formal Software Verification
University System of Maryland via edX Principles of Secure Coding
University of California, Davis via Coursera