Trace-Guided Synthesis of Effectful Test Generators
summary
Underapproximate type-and-effect specs (U-hats) plus a small typed DSL synthesize effectful test generators that interact with black-box systems rather than just produce data. The implementation, KUSO, converts a global property into a DSL skeleton, fills holes guided by local U-hats, and emits generators for QCheck and the P model checker. Evaluation shows 100% bug detection on chosen benchmarks, uses on average 3 constraints per uhat, and completes synthesis in <3s average, <3min max.
AI-written summary · about
chapters (12)
- 0:00Trace-guided synthesis intro
- 1:09What is trace-guided synthesis
- 3:36Effectful testing challenges
- 7:52API guidance with local specs
- 10:21UHats language explained
- 11:48DSL for generators & soundness
- 13:14Type-guided synthesis algorithm
- 15:01Okamo backend evaluation
- 15:44P backend evaluation
- 16:29Synthesis performance results
- 17:34Summary of contributions
- 17:56Q&A
related talks
14mSynthesizing Contracts Correct Modulo a Test Generator
19mCovering All the Bases: Type-Based Verification of Test Input Generators
28mLanguage Support for Property-Based Testing
20mDerivative-Guided Symbolic Execution
21mDependent Types to Push Corners of the Property-based Testing (Extended Abstract)
46mTesting in the world of Functional Programming
26mThe missing piece of testing
38mLiving with Spec