We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
summary
A tool called Cobb repairs incomplete OCaml input generators by synthesizing code that fills typed holes so the generator’s range includes every valid input, using coverage types to characterize missing cases and a bottom‑up cost‑guided enumerator to build repairs. The prototype is ~4.5K LOC, handles lists, trees, red‑black trees and a simply typed lambda calculus, finds precise repairs typically under a minute, and compared to coverage‑only fixes avoids producing many invalid outputs (worst case ~10% valid).
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:48Default generator problems
- 3:14Program synthesis for repair
- 5:41Cobb: coverage and safety
- 7:05Synthesis with typed holes
- 9:50Pruning unsafe terms
- 11:14Implementation benchmarks
- 13:20Lambda calculus evaluation
- 14:05Conclusion & Q&A
related talks
19mCovering All the Bases: Type-Based Verification of Test Input Generators
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
30mConstrained generation of well-typed programs
18mType-Based Incorrectness Reasoning
04mFTFY: Research advances in automatic bug repair
12mAutomatic Grammar Repair
14mLower Your Guards: A Compositional Pattern-Match Coverage Checker
21mDependent Types to Push Corners of the Property-based Testing (Extended Abstract)