ECE Seminar: Test Case Generation from Mutants using Model Checking Techniques
Tuesday, December 11, 2012 - 11:45am to 1:00pm
Heinz Riener, Ph.D Student, University of Bremen, Germany
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 test cases 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 Model Checking (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.