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.

翻译：回归测试套件是管理程序演化的关键资源，需要达到100%或接近全覆盖的覆盖率才具有实用价值。手动设计测试套件极其繁琐且不可接受，但现有自动化方法往往效率低下。本文描述的方法"播种矛盾"通过向程序的每个基本块中插入错误指令，使得基于SMT的霍尔风格验证器能够为程序的每个分支生成反例，并从所有此类反例的集合中构建测试套件。该方法采用静态分析，运行速度快，且能实现极佳的覆盖率。