Faster SAT Solving for Software with Repeated Structures (with Case Studies on Software Test Suite Minimization)

TL;DR

This paper introduces SNAP, a new approach combining clustering and theorem proving to efficiently generate minimal, valid test suites for large software, significantly reducing size and computation time.

Contribution

The paper presents SNAP, a novel technique that leverages clustering and mutation strategies with Z3 to improve test suite minimization and validity in software testing.

Findings

SNAP produced test suites 10 to 750 times smaller than previous methods.

SNAP ran orders of magnitude faster than prior approaches.

SNAP generated 100% valid tests, unlike previous work.

Abstract

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.