Testing Specifications In Dafny

on YouTube ↗17m

" summary

IronSpec provides concrete ways to surface specification bugs in Dafny: an automatic sanity checker that flags input/output disconnects, an automated mutation testing pipeline that mutates specs and keeps alive mutations whose proofs still pass, and a methodology for writing Spec-Testing Proofs (STPs) as unit-style checks. The prototype runs on nine specifications (including three open-source verified systems) and finds specification bugs in each of those three, helping distinguish specs that are too weak or too strong.

AI-written summary · about

" chapters (10)

1. 0:00Spec testing in Dafny
2. 1:04Why specs need testing
3. 2:29Verifying trusted specs
4. 3:54Iron Spec testing
5. 7:02Automatic sanity checks
6. 8:47Manual spec testing
7. 10:52Mutation testing specs
8. 13:20Iron Spec results
9. 14:21Impact on open-source
10. 15:14Q&A

" related talks

• 15mIronSpec: Increasing the Reliability of Formal SpecificationsManos Kapritsos, Eli Goldweber, Weixin Yu, Seyed Armin Vakil Ghahani · 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24)
• 38mLiving with SpecSimon Belak · EuroClojure 2016
• 47mTesting the Hard Stuff and Staying SaneJohn Hughes · Clojure/West 2014
• 20mRandomised Testing of the Dafny Compiler: Into the CIAlastair F. Donaldson, Stefan Zetzsche, Karnbongkot Boonriong · Dafny 2025
• 01h 06mBeyond Test Driven DevelopmentBurk Hufnagel · Connect.Tech 2022
• 43mspec loves data structuresMichał Marczyk · EuroClojure 2017
• 42mWorkshop / Taming Chaotic Specs: RSpec Design PatternsAdam Cuppy · Rails Pacific 2016
• 38mAbove and beyond type systems with clojure.specCarlo Sciolla · Codemotion Milan 2017