From Driller paper. Here is something about state merging in terms of symbolic execution.

1 Veritesting is a technique (using statis symbolic execution for DSE) and MergePoint is SE a system for software testing. So, there are DSE (for testing) and SSE (for verification). But! They are talking about online DSE, not concolic (offline)! Veritesting alternates between these two approaches. MergePoint is for 32-bit Linux binaries and works without debug information. 2 They begin with DSE and then switch to SSE to check program fragments for testing, not to verification. Their main success: combined approach is better on all 3 metrics: (1) number of real bugs, (2) code coverage, (3) path coverage. All metrics are important (you can have 100 % coverage but fail to find bugs) to thesis.

3 SSE techniques: Calysto and Saturn. DSE forks off two executors (and they are forever independent) but SSE can summarize the effects of both branches: all paths encoded into a single formula.

for (int i = 0; i < 100; i++) {
    if (input[i] == 'a') counter++;
}
if (counter == 75) abort();

KLEE, S²E, and Mayhem fails on above example. SSE uses dynamically recovered CFG to determine frontiers (what is easy to solve) and summarizes the effects of all path through the easy nodes up to the hard frontier. See dynamic state merging.

4 First after fork is CFG recovery: obtain partial CFG (entry point is branch). It uses BAP for recovery.

6 MergePoint is build on top of Mayhem. They use Pin for instrumentation and Z3 for solving.

Sergey Vartanov, 2007–2020