CREST is an automatic test generation tool for C.

It 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 reasons symbolically only about linear, integer arithmetic. CREST should be usable on any modern Linux system. It is usable on recent Mac OS X versions, as well, although some small modifications are needed for the code to build.

For further building and usage information, see the README file. You may also want to check out the FAQ.

Further questions? Contact Jacob Burnim (jburnim at cs dot berkeley dot edu) or e-mail the CREST-users mailing list (CREST-users at googlegroups.com).

A short paper and tech report about some of the search strategies in CREST are available at the homepage of Jacob Burnim.

News: CREST 0.1.1 is now available. It can be downloaded from the Downloads section (or the menu bar on the right). This is a bug fix release -- the biggest change is a fix for incorrect instrumentation for functions returning structures by value.