一句话：提出欠近似类型与效应系统，用符号轨迹约束引导合成测试生成器，有效探测带效应黑盒系统。
近年程序逻辑通过欠近似来推理可达性而非安全性。本文探索将类似思想融入表达性类型与效应系统，用欠近似类型规范指导合成测试生成器，以探测带副作用黑盒系统的行为。其类型语言的关键创新是用符号轨迹刻画效应操作的欠近似行为，暴露潜在的数据与控制依赖，并给出生成器输出测试序列必须保持的约束。作者实现原型工具，将合成生成器分别集成到基于属性的测试框架 QCheck 和模型检查工具 P 中，并在多种应用上评估。结果显示，合成生成器显著优于默认测试策略，且与最先进的手写方案相当。
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 , and evaluate it on a diverse range of applications by integrating ’s synthesized generators into property-based testing frameworks like QCheck and model-checking tools like P. In both settings, the generators synthesized by are significantly more effective than the default testing strategy, and are competitive with state-of-the-art, handwritten solutions.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ZhouDDJ26,
title = {Trace-Guided Synthesis of Effectful Test Generators},
author = {Zhe Zhou and Ankush Desai and Benjamin Delaware and Suresh Jagannathan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808264}
}