Building Very Small Test Suites (with Snap)
This addresses the challenge of efficient and reliable test suite generation for software engineers dealing with large-scale programs, representing a strong specific gain rather than an incremental improvement.
The paper tackled the problem of generating very small test suites for large, complex software by introducing SNAP, which combines the Z3 theorem prover with a tactic of sampling around average values from random valid tests. The result was test suites 10 to 750 times smaller than prior state-of-the-art, with orders of magnitude faster runtime and 100% valid tests for 27 real-world programs.
Software is now so large and complex that additional architecture is needed to guide theorem provers as they try to generate test suites. For example, the SNAP test suite generator (introduced in this paper) combines the Z3 theorem prover with the following tactic: sample around the average values seen in a few randomly selected valid tests. This tactic is remarkably effective. For 27 real-world programs with up to half a million variables, SNAP found test suites which were 10 to 750 smaller times than those found by the prior state-of-the-art. Also, SNAP ran orders of magnitude faster and (unlike prior work) generated 100% valid tests.