Testing Specifications in Dafny - Dafny'24

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.