KDAlloc: The KLEE Deterministic Allocator: Deterministic Memory Allocation during Symbolic Execution and Test Case Replay

ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pp. 1491–1494

Abstract

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.

Authors 5

1. Daniel Schemmel

   Imperial College London

   Affiliation as printed

   Imperial College London, UK

2. Julian Büning Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

3. Frank Busse

   Imperial College London

   Affiliation as printed

   Imperial College London, UK

4. Martin Nowack

   Imperial College London

   Affiliation as printed

   Imperial College London, UK

5. Cristian Cadar

   Imperial College London

   Affiliation as printed

   Imperial College London, UK