: A Concolic Unit Testing Engine for C
1 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 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 '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