KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs

By Cristian Cadar, Daniel Dunbar, Dawson R. Engler. 2008

3,736 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Detecting Violations of Differential Privacy (2018, background): “Symbolic execution [9, 10, 26] is widely used for program testing and bug finding.”
Deep Learning Based Vulnerability Detection: Are We There Yet? (2020, background): “While dynamic analyzers execute the program on real inputs, symbolic analyzers analyze the program based on symbolic inputs [68], [73].”
Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts (2019, methodology): “eous state setup (e.g. binary loading). Syscalls must handle symbolic inputs, yet few can be reasonably modeled symbolically. Manticore therefore concretizes system call arguments and (much like KLEE [6]) forwards such calls to the real OS. C. Ethereum Execution Module Manticore supports Ethereum sm”
Using Frankencerts for Automated Adversarial Testing of Certificate Validation in SSL/TLS Implementations (2014, methodology): “More recent work by Ramos and Engler on UC-KLEE [63], which integrates KLEE [11] and lazy initialization [45], applies more comprehensive symbolic execution over a bounded exhaustive execution space to check code equivalence; UCKLEE has been effective in finding bugs in different tools, including it”
NAUTILUS: Fishing for Deep Bugs with Grammars (2019, background): “More advanced techniques are either taint-based [24], [27], [29], [43], [50], symbolic [26], or concolic [31], [32], [46] (a portmanteau of concrete and symbolic).”
Directed Greybox Fuzzing (2017, methodology): “The state-of-the-art patch testing tool is Katch [21], a directed whitebox fuzzer that is based on the symbolic execution engine Klee [7].”
The Art, Science, and Engineering of Fuzzing: A Survey (2018, background): “2, we intentionally omit dynamic symbolic executors such as [92], [198], [63], [49], [218], [54] because their authors did not explicitly describe their work as a fuzzer.”
QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing (2018, methodology): “Concolic execution has been largely adopted for automatic vulnerability finding from source code [19, 41, 42] to binary [4, 5, 20, 21, 43].”
A NICE Way to Test OpenFlow Applications (2012, unknown): “Instead, we extend model checking to symbolically execute [17, 18] the handlers, as discussed in Section 3.”
Automated Test Case Generation as a Many-Objective Optimisation Problem with Dynamic Selection of the Targets (2018, methodology): “Other than evolutionary approaches, other techniques have been proposed in the literature for test case and test data generation, such as dynamic symbolic execution [7], [26], [53], [56] and random testing [9], [32], [36], [37].”