Concolic testing of sequential . . .

Testing using manually generated test cases is the primary technique used in industry to improve reliability of software—in fact, such ad hoc testing accounts for over half of the typical cost of software development. We propose new methods for systematically and automatically testing sequential and concurrent programs. The methods are based on two new techniques: concolic testing and race-detection and flipping. Concolic testing combines concrete and symbolic testing to automatically and systematically test sequential programs having memory graphs as inputs. Concolic testing can catch generic errors such as assertion violations, uncaught exceptions, and segmentation faults. Large real-world programs are almost always concurrent. Because of the inherent non-determinism of such programs, testing is notoriously hard. We extend concolic testing with a method called race-detection and flipping, which provides ways of reducing, often exponentially, the exploration space for concolic testing. This combined method provides the first technique to effectively test concurrent programs with complex data inputs. Based on the above methods we have developed tools for testing both C and Java programs. We have used the tools to find bugs in several real-world software systems including SGLIB, a popular C data structure library used in a commercial tool, implementations 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