Covering All the Bases: Type-Based Verification of Test Input Generators

Explore a 19-minute video presentation from the PLDI 2023 conference that introduces a novel approach to verifying test input generators for property-based testing. Learn about a new refinement type-based verification procedure that validates the coverage provided by input test generators, using "must-style" underapproximate reasoning principles embedded in the type system. Discover how this method addresses the challenge of ensuring generators produce all acceptable elements satisfying input types and constraints. Gain insights into the formalization of coverage types in a core language with higher-order procedures and inductive datatypes, and examine the evaluation study demonstrating the utility of this approach. Delve into the intersection of refinement types, property-based testing, and underapproximate reasoning to enhance the reliability and effectiveness of software testing practices.