KLEEF: Symbolic Execution Engine (Competition Contribution)
Aleksandr Misonizhnik, Sergey Antonovich Morozov, Yurii Kostyukov, Vladislav Kalugin, Alexey Alexandrovich Babushkin, Dmitry Mordvinov, Dmitry Ivanov · Lecture notes in computer science · 2024
Abstract KLEEF is a complete overhaul of the KLEE symbolic execution engine for LLVM, fine-tuned for a robust analysis of industrial C/C++ code. KLEEF natively handles complex data structures, such as trees, linked lists, and dynamically allocated arrays, via lazy initialization and symcrete values. KLEEF has fine-tuned modes for both maximal test coverage generation and reproducing error traces, in particular reaching a specific point in the program. In the paper, we describe the above features and a competition configuration of KLEEF.