Automated Test Generation Using Concolic Testing

In this talk, I will describe concolic testing, also known as directed automated random testing (DART) or dynamic symbolic execution, 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. 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.