Concolic StarFinder (JSF) is a unit test generation tool for programs that make extensive use of dynamically allocated data structures such as lists and trees. Users need to provide a precondition, an inductive predicate in separation logic, to describe the input data structure. CSF then performs mix of concrete and symbolic, or concolic, execution on the program to generate test cases, and use the precondition to guide its search.
- Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun. Concolic Testing Heap-Manipulating Programs. FM 2019. [PDF]
For common questions, bug reports, and feature requests, please use the JPF Google Group.
Suppose you are in the root directory of jpf-costar, simply run:
$ bin/testAll.sh