Symbolic execution for software testing: three decades later

Cristian Cadar, Koushik Sen

  • Read: 20 Apr 2025
  • Published: 01 Feb 2013

Communications of the ACM, Volume 56, Issue 2 Pages 82 - 90

https://doi.org/10.1145/2408776.2408795

See also: KLEE, EXE.

Apparently the author Cristian Cadar is actively working in the area of symbolic execution, he is also one of the authors of EXE: Automatically Generating Inputs of Death.

Compared to this survey, A Survey of Symbolic Execution Techniques might be a more detailed one to read.

When skimming the survey Symbolic execution for software testing: Three decades later I came accross a section named “Tools” which listed many symbolic execution tools with a brief introduction. I summarized them as below:

  1. DART: The first concolic testing tool that combines dynamic test generation with random testing and model checking techniques with the goal of systematically executing as many as possible execution paths of a program. DART was first implemented at Bell Labs for testing C programs, and has inspired many other extensions and tools since.
  2. CUTE: Extends DART to handle multithreaded programs that manipulate dynamic data structures using pointer operations. Developed at UIUC for C and Java programs (jCUTE is dedicated to Java).
  3. CREST: An open-source tool for concolic testing of C programs. It is an extensible platform for building and experimenting with heuristics for selecting which paths to explore.
  4. EXE: A symbolic execution tool for C programs designed for comprehensively testing complex software, with an empasis on systems code. EXE models memory with bit-level accuracy. EXE provides the speed necessary to quickly solve the constraints generated by real code, through a combination of low-level optimizations implemented in its purposely designed constraint solver STP, and a series of higher-level ones such as caching and irrelevant constraint elimination.
  5. KLEE: A redesign of EXE, built on top of the LLVM-compiler infrastructure. It performs concolic execution, models memory with bit-level accuracy, employs a variety of solving optimizations, and uses search heuristics to get high code coverage. one of the key improvements of KLEE over EXE is its ability to store a much larger number of concurrent states, by exploiting sharing among states at the object-level rahter than at the page-level. KLEE also has better environment interaction than EXE.
  6. SAGE: A dynamic symbolic execution tool developed by Microsoft for x86 binaries.
Written on