Type-Based Incorrectness Reasoning
summary
Claims that coverage types extend refinement types to give underapproximate reasoning that verifies completeness of nondeterministic test generators, and shows a direct encoding into a simple nondeterministic lambda where an added random initialization simulates test generation. Uses product/result types to label OK/error runs, and mixes over- and under-approximate parameter types to express “for all” vs “exists” inputs. Works on the worked examples but requires termination proofs (structural decreases) and faces specification tradeoffs.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:25Type-based incorrectness reasoning
- 1:27Coverage types purpose
- 3:35Coverage types syntax
- 5:44Coverage types subtyping
- 6:47Coverage vs incorrectness verification
- 7:54Incorrect verification explained
- 10:04Tracking correct and error executions
- 11:30Function types and parameters
- 13:58Balancing approximation types
- 14:40Summary and future work
- 15:23Q&A
related talks
19mCovering All the Bases: Type-Based Verification of Test Input Generators
51mWhen Types are Not Enough
45mTDD, as in Type-Directed Development
20mType-level Property Based Testing
44mTypes and Property Tests for Software Resiliency
36mProperty-Based Testing: Unveiling the Truth on Test Reduction
46mTesting in the world of Functional Programming
16mWe’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators