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

Dec 11

Tuesday, December 11, 2012

Presenter

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.

Contact

Currin, Ellen
660-5252
ecurrin@ee.duke.edu