CREST

Concolic test generation tool for C

View project onGitHub

CREST is an 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.

Further questions? Please e-mail the CREST-users mailing list (CREST-users at googlegroups.com, searchable at https://groups.google.com/forum/#!forum/crest-users).

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

News: CREST 0.1.2 is now available. It can be downloaded at https://github.com/jburnim/crest/releases/tag/v0.1.2. This is a bug fix release -- several build issues are fixed, as well as a bug in instrumenting unary expressions.

News: Heechul Yun has extended CREST to support non-linear arithmetic (using Z3). For more information, see: https://github.com/heechul/crest-z3 and https://github.com/heechul/crest-z3/blob/master/README-z3.