Bertrand Meyer's technology+ blog

Just published: Li Huang, Bertrand Meyer and Manuel Oriol, Seeding Contradiction: a fast method for generating full-coverage test suites, in Springer Nature Computer Science, vol. 6, no. 4, 2025. The text is available here on the publisher’s site. Also available is a preprint version.

This just published SNCS article and revised and extended from a conference presentation (at ICTSS 2023 in Bergamo, see here on my efforts back then to use AI to locate the conference site). It describes a new and promising test generation method, part of systematic effort at combining tests and proofs, highlighted in the recent PhD defense of Li Huang (about which I did not have the time to write an article, but will soon).

A new method for achieving full test coverage, very fast, without execution. The idea is to insert an incorrect instruction in every path of the program (technically, every basic block). Then, attempt to prove the program correct, using an SMT-solver-based prover. We “seed a contradiction” into the program.

The proof will fail, as expected, but the solver will generate a counter-example which we can turn into a test using the techniques first presented in earlier papers, including this article. The resulting set of tests is guaranteed to achieve 100% coverage! As a matter of fact the result is better than what is usually understood as “full coverage” since in this journal version we have added the possibility of unrolling loops. (Branch coverage and other usual techniques treat a loop as a conditional, executed either once or not at all. We can execute the body several times, based on a provided parameter.)

Caveat: the examples are still fairly small, although some of them are intricate. Even in this current state, the approach and tool hold the promise of using modern program-proving technology to generate, fully automatically, exhaustive test suites.

Reminder: my full annotated publication list is here.

Be Sociable, Share!

• 
•