KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs

We present a new symbolic execution tool, KLEE, ca-pable of automatically generating tests that achieve high coverage on a diverse set of complex and environmentally-intensive programs. We used KLEE to thoroughly check all 89 stand-alone programs in the GNU COREUTILS utility suite, which form the core user-level environment installed on millions of Unix sys-tems, and arguably are the single most heavily tested set of open-source programs in existence. KLEE-generated tests achieve high line coverage — on average over 90% per tool (median: over 94%) — and significantly beat the coverage of the developers ’ own hand-written test suites. When we did the same for 75 equivalent tools in the BUSYBOX embedded system…