Compositional Generator Equivalence (Extended Version) (opens in new tab)

Property-based testing (PBT) is a powerful technique for software verification that relies on random input generators and "shrinking" processes to find and minimize counterexamples to executable specifications called properties. While optimizing these generators is crucial for testing efficiency, formally justifying such optimizations is currently difficult because existing languages lack a compositional semantics that is coarse-grained enough f...