Accession Number:

AD1006571

Title:

Interprocedural Analysis and the Verification of Concurrent Programs

Descriptive Note:

Technical Report

Corporate Author:

University of Wisconsin Madison United States

Personal Author(s):

Report Date:

2009-01-01

Pagination or Media Count:

252.0

Abstract:

In the modern world, not only is software getting larger and more complex, it is also becoming pervasive in our daily lives. On the one hand, the advent of multi-core processors is pushing software towards becoming more concurrent, making it more complex. On the other hand, software is everywhere, inside nuclear reactors, space shuttles, cars, traffic signals, cellphones, etc. To meet this demand for software, we need to invest in automated program verification techniques, which ensure that software will always behave as intended.The problem of program verification is undecidable. A verification technique can only gain a limited amount of knowledge about a programs behavior by reasoning about certain aspects of the program. This dissertation addresses program verification by considering two important features of programs i procedures and procedure calls and ii concurrency. Interprocedural Analysis An analysis that can precisely handle the procedural aspect of programs is called an interprocedural analysis. Procedures are an important feature of most programming languages because they allow for modular design of programs each procedure is meant to perform a task, and they can be put together to implement more complex functionality. Because procedures serve as a natural abstraction mechanism for developers to organize their programs, an interprocedural analysis can leverage them to enable verification of a larger and more complex programs.There is a long history of work on interprocedural analysis, including several frameworks that support a variety of different program abstractions, and provide algorithms for analyzing them. The advantage of having a framework is that any program abstraction that fits the framework can make use of the algorithms for the framework. One such framework, called Weighted Pushdown Systems WPDSs, was the subject of the research reported on in this dissertation.

Subject Categories:

Distribution Statement:

APPROVED FOR PUBLIC RELEASE