Faster SAT Solving for Software with Repeated Structures (with Case Studies on Software Test Suite Minimization)
This work provides a significant improvement in the efficiency and effectiveness of test suite generation for software engineers dealing with large and complex software.
The paper introduces SNAP, a test suite generator that combines the Z3 theorem prover with a clustering and mutation tactic to handle repeated structures in software. SNAP generated test suites 10 to 750 times smaller and ran orders of magnitude faster than prior state-of-the-art methods for 27 real-world programs, while also producing 100% valid tests.
Theorem provers has been used extensively in software engineering for software testing or verification. However, software is now so large and complex that additional architecture is needed to guide theorem provers as they try to generate test suites. The SNAP test suite generator (introduced in this paper) combines the Z3 theorem prover with the following tactic: cluster some candidate tests, then search for valid tests by proposing small mutations to the cluster centroids. This technique effectively removes repeated structures in the tests since many repeated structures can be replaced with one centroid. In practice, SNAP 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.