KDAlloc: The KLEE Deterministic Allocator: Deterministic Memory Allocation during Symbolic Execution and Test Case Replay
Authors: 
Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, 
Cristian CadarAuthors Info & Claims
Pages 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.
References
[1]
Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI’08.
[2]
Cristian Cadar and Dawson Engler. 2005. Execution Generated Test Cases: How to Make Systems Code Crash Itself. In SPIN’05. https://doi.org/10.1007/11537328_2
[3]
Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. CACM, 56, 2 (2013), 82–90. https://doi.org/10.1145/2408776.2408795
[4]
Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliff Stein. 2001. Introduction to Algorithms (second ed.). MIT Press/McGraw Hill.
[5]
Jason Evans. 2006. A Scalable Concurrent malloc(3) Implementation for FreeBSD. In BSDCan’06.
[6]
Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed Automated Random Testing. In PLDI’05.
[7]
James C. King. 1976. Symbolic Execution and Program Testing. CACM, 19, 7 (1976), 385–394.
[8]
[n. d.]. KLEE website. http://klee.github.io/
[9]
Chris Lattner and Vikram Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In CGO’04. https://doi.org/10.1109/CGO.2004.1281665
[10]
Nicholas Nethercote and Julian Seward. 2003. Valgrind: A Program Supervision Framework. Electronic Notes in Theoretical Computer Science, 89, 2 (2003).
[11]
Mark E. Russinovich, David A. Solomon, and Alex Ionescu. 2012. Windows® Internals, Part 2 (6th ed.). Microsoft Press. isbn:9780735677272
[12]
Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, and Cristian Cadar. 2022. A Deterministic Memory Allocator for Dynamic Symbolic Execution. In ECOOP’22. https://doi.org/10.4230/LIPIcs.ECOOP.2022.9
[13]
Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitry Vyukov. 2012. AddressSanitizer: A Fast Address Sanity Checker. In USENIX ATC’12.
Index Terms
- KDAlloc: The KLEE Deterministic Allocator: Deterministic Memory Allocation during Symbolic Execution and Test Case Replay
Recommendations
Test Case Selection Based on Path Condtions of Symbolic Execution
APSEC '12: Proceedings of the 2012 19th Asia-Pacific Software Engineering Conference - Volume 01Symbolic execution as a test case generation technique has recently become an active research area. However, since symbolic execution generates a large number of test cases, it is impractical to run all the generated test cases in practice. In this ...
Handling Memory-Intensive Operations in Symbolic Execution
ISEC '22: Proceedings of the 15th Innovations in Software Engineering ConferenceSymbolic execution is a popular software testing technique that can help developers identify complex bugs in real-world applications. Unfortunately, symbolic execution may struggle at analyzing programs containing memory-intensive operations, such as ...
Using test case reduction and prioritization to improve symbolic execution
ISSTA 2014: Proceedings of the 2014 International Symposium on Software Testing and AnalysisScaling symbolic execution to large programs or programs with complex inputs remains difficult due to path explosion and complex constraints, as well as external method calls. Additionally, creating an effective test structure with symbolic inputs can ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2023
1554 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 13 July 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
ISSTA '23
Sponsor:
ISSTA '23: 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis
July 17 - 21, 2023
WA, Seattle, USA
Acceptance Rates
Overall Acceptance Rate 58 of 213 submissions, 27%
Upcoming Conference
ISSTA '25
- Sponsor:
- sigsoft
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 542Total Downloads
- Downloads (Last 12 months)365
- Downloads (Last 6 weeks)58
Reflects downloads up to 01 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in