Seeding Contradiction: a fast method for generating full-coverage test suites

TL;DR

Seeding Contradiction is a fast, static method that uses SMT-based reasoning to generate comprehensive test suites with high coverage by producing counterexamples for every branch.

Contribution

It introduces a novel static approach that efficiently generates full-coverage test suites using SMT solvers and program contradiction seeding.

Findings

Achieves near 100% branch coverage

Fast and static method for test generation

Effective for large and complex programs

Abstract

The regression test suite, a key resource for managing program evolution, needs to achieve 100% coverage, or very close, to be useful. Devising a test suite manually is unacceptably tedious, but existing automated methods are often inefficient. The method described in this article, ``Seeding Contradiction'', inserts incorrect instructions into every basic block of the program, enabling an SMT-based Hoare-style prover to generate a counterexample for every branch of the program and, from the collection of all such counterexamples, a test suite. The method is static, works fast, and achieves excellent coverage.