Covering All the Bases: Type-Based Verification of Test Input Generators
summary
Claims a new coverage types system that interprets refinements as underapproximate reasoning and verifies whether generators actually produce every value in a target set. Implements a prototype called Pearl (OCaml) that uses Z3 for SMT subtyping, formalizes soundness for higher-order and inductive datatypes, and checks 14 handwritten generators (lists, trees, heaps, sets). Type checking stays under ~13s on benchmarks; empirical result shows 76–99% of previously “safe” generators fail the coverage check.
AI-written summary · about
chapters (14)
- 0:00Type-based verification intro
- 1:48Coverage vs safety verification
- 3:14Coverage types solve problem
- 6:25Differences from refinement types
- 8:12Control flow in coverage types
- 9:38Function types for approximations
- 11:03Formalization and soundness
- 11:45Pearl typing algorithm
- 12:08Pearl effectiveness eval
- 12:51Pearl efficiency benchmarks
- 13:34Pearl scalability case study
- 13:57Coverage vs safety types utility
- 15:26Summary and artifacts
- 15:53Q&A
related talks
18mType-Based Incorrectness Reasoning
16mWe’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
51mWhen Types are Not Enough
21mDependent Types to Push Corners of the Property-based Testing (Extended Abstract)
26mThe missing piece of testing
30mConstrained generation of well-typed programs
21mTrace-Guided Synthesis of Effectful Test Generators
33mLets Generate Tests