Scalable Automated Methods for Dynamic Program Analysis

Sen, Koushik

Permalink

https://hdl.handle.net/2142/11198 Copy

Description

Title

Scalable Automated Methods for Dynamic Program Analysis

Author(s)

Sen, Koushik

Issue Date

2006-06

Keyword(s)

computer science

Abstract

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 three new techniques: concolic testing, race-detection and flipping, and predictive monitoring. Concolic testing combines concrete and symbolic testing to avoid redundant test cases as well as false warnings. 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. Concolic testing may also be combined with formal specifications by using runtime monitors. Runtime monitors are small software units which are synthesized automatically from the formal specification for the software and weaved into the code to dynamically check if the specification is violated. For multi-threaded concurrent programs, we developed a novel technique which allows efficient predictive monitoring to enable the detection of a violation by observing some related, but possibly bug-free execution of a concurrent program. Predictive monitoring dramatically improves the efficiency of testing. 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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11198

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections