KDAlloc: The KLEE Deterministic Allocator


The memory allocator can have an important impact in symbolic execution.
Taking a user-centric view, this tool demonstration paper discusses some of the main benefits provided by KLEE’s new allocator KDAlloc in terms of improved deterministic execution and bug-finding capabilities.
We then introduce a new replay tool for KLEE which enables the native execution to integrate KDAlloc and receive the same heap addresses as during symbolic execution.