Concolic testing

Author:
Open Access
Publisher website
Google Scholar
Abstract
Concolic testing automates test input generation by com- bining the concrete and symbolic (concolic) execution of the code under test. Traditional test input generation tech- niques use either (1) concrete execution or (2) symbolic exe- cution that builds constraints and is followed by a generation of concrete test inputs from these constraints. In contrast, concolic testing tightly couples both concrete and symbolic executions: they run simultaneously, and each gets feedback from the other. We have implemented concolic testing in tools for test- ing both C and Java programs. We have used the tools to nd bugs in several real-world software systems including SGLIB, a popular C data structure library used in a com- mercial tool, a third-party implementation of the Needham- Schroeder protocol and the TMN protocol, the scheduler of Honeywell's DEOS real-time operating system, and the Sun Microsystems' JDK 1.4 collection framework. In this tuto- rial, we will describe concolic testing and some of its recent extensions.