1 Tool Splat. Path explosion can be alleviated by performing test generation compositionally (link to this paper). Their approach is less precise but much faster than normal symblic execution: it is an approach to search space pruning. String is just a buffer with string content. 2 Main idea: track buffers and string partially symbolically, use symbolic prefix and fill buffer beyond prefix with random. For each pointer they have valid range (addresses can be safely accessed by the pointer, e.g. bounds for a pointer into a buffer). For each memory dereference they write danger condition. 3 Partial symbolic representation can miss path, but you always can increase symbolic prefix size.

They analyze program on the source level. So, they don't bind symbolic variables of string prefix to real memory cells. Thus, they just use non-zero characters and add terminator.

5 Splat is for C programs, it uses source-to-source instrumentation. 6 Memory nodes are sorted by address ranges using a splay tree (self-adjusting binary search tree). They replace functions in string.h with their string library (own string library!) that is aware of symbolic length and memory nodes. Splat use different search strategies. They looks for memory violations like Valgrind's Memcheck. But they can always detect buffer overflows that overwrite the return address. They also use more precise asserts. 7 For solving they use STP (bit-accuracy of STP matter). They have a real exploit benchmarks.

Sergey Vartanov, 2007–2020