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

Dec 11

This event has passed.

Tuesday, December 11, 2012 - 11:45am to 1:00pm

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.