2 Their framework is UC-KLEE. For checking C/C++ code. They check patches for chashes introducing. Patches intended to fix bugs are frequent source of them. 3 UC-KLEE can verify that patch does not introduce new crashes. 3 checkers: memory leaks, uses of uninitialized, unsanitized uses of user input. On one function it can exhaust all paths. UC-KLEE executes functions without preconditions, so this under-constraining may cause false positives. Has FP, but still verify code. Function's symbolic input generation uses lazy initizlization. 4 Limitations: only check patches that do not reorder fields in data structures. 5 UC-KLEE symbolically executes both patched and unpatched versions and report defect iff it occures in patched version and not occured in unpatched (if crash was in unpatched version, it is likely a FP). They have previous paper about function equivalence.

For path pruning it has static cross-checker. It walks over CFG and mark BB that differs. So, not patched paths will be pruned. Also it prunes pathses that has no error or has error without reaching differing blocks.

evaluate skipped

14 They use symbolically-sized objects. Inputs for one function checking is more complex that command-line and input files for whole program. It hard to be created by user and hard to reproduce automatically. 15 So, UC-KLEE emits a path summary for each error with complete source code listing with PC. They found query timeouts due to symbolic division and remainder operations. Their solution—lazy constraints. They postpone evaluation of expensive constraints until error is found:

int x = y / z; // lazy_x = y / z
if (x > 10)    // lazy_x > 10

Complex C-systems frequently use function pointers within struct types to emulate OO methods. So, there is indirect calls problem. Their solution: require that users specify concrete function pointers to associate with each type of object.

Sergey Vartanov, 2007–2020