Title: Coverage Types: Underapproximate Refinement Types for Generator Coverage

Speaker: Ashish Mishra    (bio) (bio)

Ashish Mishra obtained his PhD from IISc Bangalore. He was subsequently a post-doctoral researcher at Northeastern University and Purdue University, before joining IIT Hyderabad as an Assistant Professor in 2024. Ashish's research interests are broadly in Program Verification and Synthesis, Functional Programming and Type Systems.

When: Tuesday, 07 April 2026 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
Property-based testing (PBT) has become a widely used technique for validating semantic properties of programs by automatically generating test inputs that satisfy user-specified preconditions. In practice, however, the effectiveness of PBT depends critically on the quality of input generators. When preconditions describe rich structural constraints, purely random generators rarely produce many valid inputs, forcing developers to write specialized generators by hand. Unfortunately, such generators are often incomplete, i.e., they may fail to produce many valid inputs, limiting the behaviors explored during testing. However, it is not readily apparent how to validate whether a particular generator provides sufficient coverage against a given precondition. Typically, developers must rely on manual inspection and post-hoc analysis.

In this talk, I will present a refinement type-based framework for reasoning about the coverage of test input generators. Our key idea is coverage types, an interpretation of refinement types that captures must-style guarantees about the values a program will produce, rather than the traditional may-style approximation of possible outputs. Conceptually, coverage types bring ideas from Incorrectness logic and underapproximate reasoning into the type system. The types associated with expressions now capture the set of values guaranteed to be produced by an expression, rather than the typical formulation that uses types to represent the set of values an expression may produce. This automated, underapproximate reasoning mechanism allows us to formally verify coverage properties of generators in a higher-order functional language with inductive data types.

Building on this foundation, I will also describe a synthesis-based program repair technique that automatically patches incomplete generators by enumerating candidate repairs guided by coverage types. Together, these ideas enable both verification and automated repair of test generators, providing stronger guarantees about the effectiveness of property-based testing and illustrating how incorrectness-style, underapproximate reasoning can be integrated with modern type systems to support practical testing workflows.