IronSpec: Increasing the Reliability of Formal Specifications
Talkat 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) · 2024-07-10..07-12·
summary
IronSpec combines automated sanity checker heuristics, a manual methodology for writing SpecTesting Proofs (STPs), and automated mutation testing as an extension of Daphne. It applies sanity checks to detect input/output disconnects, uses STPs to turn failing obligations into concrete counterexamples, and generates syntactic spec mutants to find alive mutations. Evaluation runs on 14 specs (six real-world verified systems) and uncovers 10 specification bugs, showing the framework reliably flags spec mismatches.
AI-written summary · about
chapters (9)
- 0:00IronSpec and spec testing
- 2:29Why specs need rigorous testing
- 3:51IronSpec framework overview
- 6:16Design principles behind IronSpec
- 8:43Manual spec testing proofs
- 11:30Testing specs at any stage
- 12:57Mutation testing for spec bugs
- 13:39Evaluation results and impact
- 14:42Q&A
related talks
17mTesting Specifications In Dafny
38mLiving with Spec
47mTesting the Hard Stuff and Staying Sane
17mSignature Inference for Functional Property Discovery
01h 08mIndustrial Strength Testing for Complex Software
29mHow Good Is Your Formal Specification Mutation Testing To The Rescue!
42mWorkshop / Taming Chaotic Specs: RSpec Design Patterns
31mInfrastructure and Environment Testing with InSpec