Symbolic execution for software testing: Three decades later

Cristian Cadar, Koushik Sen
[doi] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 27 June 2020

Communications of the ACM 56(2)
Association for Computing Machinery
New York, NY, USA
Pages 82-90
February 2013
Note(s): symbolic execution, DART verifier, KLEE verifier, EXE verifier, CUTE verifier, CREST verifier, survey
Papers: baldoni:compsurv:2018

This is a survey of symbolic execution with an emphasis on the KLEE verifier. It is probably a better introduction to the concepts of symbolic execution than the baldoni:compsurv:2018 survey but this makes it less complete.

Like baldoni:compsurv:2018, this article describes some of the important optimizations to make symbolic execution effective including

  • Path optimizations such as random exploration, interleaving symbolic execution with random exploration, pruning redundant paths, lazy test generation (only exploring functions if their output is important to the constraint), static path merging (aka branch predication).

  • Constraint optimizations such as irrelevant constraint elimination, incremental solving (e.g., counterexample caching),

It ends with a sketch of five symbolic execution tools: the DART verifier, CUTE, CREST, EXE and the KLEE verifier.

KLEE verifier