Generating Good Generators for Inductive Relations

Watch a 20-minute conference presentation from POPL 2018 exploring how to automatically generate effective test data for property-based random testing in Coq. Learn about a novel compilation technique that produces certified generators for inductive relations, building upon narrowing concepts while avoiding interpretive overhead. Discover how the presenters implemented this approach as an extension to QuickChick, demonstrating its practical application by automatically deriving sound and complete generators for specifications from Software Foundations. The talk covers key concepts in random testing, property-based testing, and formal verification, with particular focus on the Coq proof assistant and QuickCheck testing framework.