Abstract

We define an automated behavioral approach to unit test generation for C code based on three steps: (1) predicate abstraction of the C code generates a boolean abstraction based on a set of observations (predicates); (2) reachability analysis of the boolean abstraction computes an overapproximation to the set of observable states and generates a small set of paths to cover these states; (3) SAT-based symbolic execution of the C code generates tests to cover the paths. Our approach generalizes a variety of test generation approaches based on covering code and deals naturally with the difficult issue of infeasible program paths that plagues many code-based test generation strategies. We explain our approach via a case study of generating test data for a small program and discuss its capabilities and limitations.