ECE Seminar: Test Case Generation from Mutants using Model Checking Techniques

Mutation testing is a powerful testing technique: a program is seeded with artificial faults and tested. Undetected faults can be used to improve the test bench. The problem of automatically generating testcases from undetected faults is typically not addressed by existing mutation testing systems. We propose a symbolic procedure for the generation of test cases from a given program using Bounded ModelChecking (BMC) techniques. The procedure determines a test bench, that detects all seeded faults affecting the semantics of the program, with respect to a given unrolling bound. We have built a prototype tool that uses a Satisfiability Modulo Theories (SMT) solver to generate test cases and we show initial results for ANSI-C benchmark programs.