A Deterministic Memory Allocator for Dynamic Symbolic Execution


Dynamic symbolic execution (DSE) has established itself as an effective testing and analysis technique. While the memory model in DSE has attracted significant attention, the memory allocator has been largely ignored, despite its significant influence on DSE.

This talk presents the design space for a memory allocator specifically designed for DSE in general, and KLEE, a popular DSE engine, in specific. The evaluation shows that our allocator, KDAlloc, is competitive with KLEE’s default allocator in terms of performance and memory overhead, and in fact significantly improves performance in several cases.

Video of the talk