CREST

CREST - automatic test generation tool for C. CREST works by inserting instrumentation code (using CIL) into a target program to perform symbolic execution concurrently with the concrete execution. The generated symbolic constraints are solved (using Yices) to generate input that drive the test execution down new, unexplored program paths. CREST currently only reasons symbolically about linear, integer arithmetic. CREST should be usable on any modern Linux or Mac OS X system. For further building and usage information, see the README file. You may also want to check out the FAQ.