Concolic testing, also known as directed automated random testing (DART) or dynamic symbolic execution, is an efficient way to automatically and systematically generate test inputs for programs. Concolic testing uses a combination of runtime symbolic execution and automated theorem proving techniques to automatically generate non-redundant and exhaustive test inputs. Specifically, concolic testing performs symbolic execution along a concrete execution path, generates a logical formula denoting a constraint on the input values, and solves a constraint to generate new test inputs that would execute the program along previously unexplored paths.
A key goal of concolic testing in the context of software testing is to explore as many different program paths as possible in a given amount of time, and for each path to (1) generate a set of concrete input values exercising that path, and (2) check for the presence of various kinds of errors including assertion violations, uncaught exceptions, security vulnerabilities, and memory corruption. The ability to generate concrete test inputs is one of the major strengths of concolic testing: from a test generation perspective, it allows the creation of high-coverage test suites, while from a bug-finding perspective, it provides developers with a concrete input that triggers the bug, which can be used to confirm and debug the error independently of the symbolic execution tool that generated it.
Concolic testing has inspired the development of several industrial and academic automated testing and security tools such as PEX, SAGE, and YOGI at Microsoft, Apollo at IBM, Conbol at Samsung, and CUTE, jCUTE, CATG, Jalangi, SPLAT, BitBlaze, jFuzz, Oasis, and SmartFuzz in academia. A central reason behind the wide adoption of concolic testing is that, while concolic testing uses program analysis and automated theorem proving techniques internally, it exposes a testing usage model that is familiar to most software developers.