Up

CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools (Tools Paper)

<span class=abbr>CUTE</span> and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools (Tools Paper)
1 · 2

1 CUTE is for C and jCUTE is for Java programs. They calls DSE symbolic execution, and pure symbolic execution traditional symbolic execution. They use term symbolic constraint for constraint from branch point to branch point, and path constraint for the conjunction of these constraints. 2 They also computes race conditions.

At every iteration they either (1) generate new input based on solving symbolic constraints or (2) generate new schedule based on re-ordering the events involved in a race. They use term sound as “without false positives”. They also use replacing some symbolic values with concrete ones to simplify constraints. Try it.

CUTE and jCUTE use CIL (C intermediate language), Soot (Java optimization framework), and lp_solve for constraints solving.

Sergey Vartanov, 2007–2020