植入矛盾：一种快速生成全覆盖测试套件的方法
Seeding Contradiction: a fast method for generating full-coverage test suites
AI总结：
针对回归测试套件全覆盖生成效率低的问题，提出静态方法Seeding Contradiction，通过在基本块植入错误指令并利用SMT证明器生成反例，快速构建全覆盖测试套件。
摘要：
回归测试套件是管理程序演化的关键资源，需达到100%或极接近的覆盖率才能发挥作用。手动设计测试套件极其繁琐，而现有自动化方法往往效率低下。本文提出的方法“Seeding Contradiction”，在程序的每个基本块中插入错误指令，使基于SMT的Hoare风格证明器为程序的每个分支生成反例，并由所有反例的集合构成测试套件。该方法为静态方法，运行速度快，且实现了出色的覆盖率。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
