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.

翻译：近期提出的若干程序逻辑已将欠逼近概念融入其设计，使其能够推理可达性而非安全性。本文探索如何将类似思想集成到富有表现力的类型与效应系统中，并利用由此产生的欠逼近类型规范来指导测试生成器的综合，以探测含效应黑盒系统的行为。我们类型语言的关键创新在于：通过符号化迹（迹可暴露潜在的数据依赖与控制依赖）捕获含效应操作的欠逼近行为，同时确保生成器输出的测试序列必须满足这些约束约束。我们在名为Clouseau的工具中实现了该方法，并通过将Clouseau综合的生成器集成到基于属性的测试框架（如QCheck）和模型检验工具（如P）中，在多样化的应用场景上进行了评估。在这两种设置下，Clouseau综合的生成器均显著优于默认测试策略，且与最新的人工编写解决方案相比具有竞争力。