Trace-Guided Synthesis of Effectful Test Generators
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910105542328320 |
|---|---|
| author | Zhou, Zhe Desai, Ankush Delaware, Benjamin Jagannathan, Suresh |
| author_facet | Zhou, Zhe Desai, Ankush Delaware, Benjamin Jagannathan, Suresh |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_04345 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Trace-Guided Synthesis of Effectful Test Generators Zhou, Zhe Desai, Ankush Delaware, Benjamin Jagannathan, Suresh Programming Languages 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. |
| title | Trace-Guided Synthesis of Effectful Test Generators |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2604.04345 |