Seeding Contradiction: a Fast Method for Generating Full-Coverage Test Suites

The regression test suite, a key resource for managing program evolution, needs to achieve 100% branch coverage, or very close, to be useful. Devising a test suite manually is unacceptably tedious. Although many automated methods exist to improve the efficiency of test generation, they are mostly dynamic. 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 full coverage, even going beyond the usual concept of branch coverage by “unrolling” loops a parameterizable number of times.