Concolic testing

Its main focus is finding bugs in real-world software, rather than demonstrating program correctness.

A description and discussion of the concept was introduced in "DART: Directed Automated Random Testing" by Patrice Godefroid, Nils Klarlund, and Koushik Sen.[1] The paper "CUTE: A concolic unit testing engine for C",[2] by Koushik Sen, Darko Marinov, and Gul Agha, further extended the idea to data structures, and first coined the term concolic testing.

[7] It was also combined with fuzz testing and extended to detect exploitable security issues in large-scale x86 binaries by Microsoft Research's SAGE.

One such tool is ExpliSAT by Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening and Ishai Rabinovitz[10] Implementation of traditional symbolic execution based testing requires the implementation of a full-fledged symbolic interpreter for a programming language.

This idea of simplifying implementation of symbolic execution gave birth to concolic testing.

An important reason for the rise of concolic testing (and more generally, symbolic-execution based analysis of programs) in the decade since it was introduced in 2005 is the dramatic improvement in the efficiency and expressive power of SMT Solvers.

Concolic testing has a number of limitations: Many tools, notably DART and SAGE, have not been made available to the public at large.

Execution path tree for this example. Three tests are generated corresponding to the three leaf nodes in the tree, and three execution paths in the program.