Several recently proposed program logics have
incorporated notions of underapproximation into their
design, enabling them to reason about
reachability rather than safety. In this paper,
we explore how similar ideas can be integrated
into an expressive type and effect system. We
use the resulting underapproximate type
specifications to guide the synthesis of test
generators that probe the behavior of effectful
black-box systems. A key novelty of our type
language is its ability to capture
underapproximate behaviors of effectful
operations using symbolic traces that expose
latent data and control dependencies,
constraints that must be preserved by the test
sequences the generator outputs. We implement
this approach in a tool called Clouseau, and
evaluate it on a diverse range of applications
by integrating Clouseau’s synthesized generators
into property-based testing frameworks like
QCheck and model-checking tools like P. In both
settings, the generators synthesized by Clouseau
are significantly more effective than the
default testing strategy, and are competitive
with state-of-the-art, handwritten solutions.