Concolic testing.

solving optimizations

1 CUTE is for automating unit testing with memory graphs as inputs (because function may contain pointer arguments) using concolic execution. First using of word concolic: concrete + symbolic. Unit testing requires input values specification (test inputs) for each unit. They want to create such specifications automatically using symbolic execution. CUTE is for C code.

Program is decomposed into units: collection of funcitons. They said first combining concrete and symbolic execution is in High coverage detection of input-related security faults by E. Larson and T. Austin.

2 They use Dart's approach. But what about pointers? They may have aliases. So, they approximate pointer constraints. Input is a logical input map. Logical input map is only needed for one function analysis? Or it's because the pointer arithmetic itself? Actually, is it a problem for all programming languages or for those which has pointer arithmetic? They instrument code by inserting function calls.

2 symbolic states:

• one for pointer values
• and one for primitive (e.g. integer) values.

Explicit path model-checking. CUTE is for concolic unit testing engine.

Here is incremental solving technique.

Sergey Vartanov, 2007–2020