Evaluating Soundness of a Gradual Verifier with Property Based Testing
summary
An empirical checker implements Gradual C0 and a fully dynamic Dynamic C0 verifier, runs both on mutated versions of a dozen large benchmarks, and asserts equivalence using the dynamic verifier as ground truth. Property-based testing generated incorrect-spec programs and found four substantive soundness bugs (matching issues from the tool’s tracker) that escape static proofs but fail at runtime, demonstrating the implementation is imperfect; an automated generator for failing gradual-C0 inputs is the next engineering step.
AI-written summary · about
chapters (5)
- 0:00Introduction
- 0:34What is Gradual Verification
- 7:26Property Based Testing
- 11:05Implementation Issues
- 12:46Future Work
related talks
42mSurprise yourself with Property Based Testing
15mGradual Verification of Recursive Heap Data Structures
14mVerify, but test: extracting property-based tests from F* specifications
47mProperty-Based Testing
19mCovering All the Bases: Type-Based Verification of Test Input Generators
26mThe missing piece of testing
38mThe Verification of a Distributed System
18mProperty-based testing beginning with SwiftCheck