Interprocedural Analysis and the Verification of Concurrent Programs
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2009
- Accession Number
- AD1006571
Entities
People
- Akash Lal
Organizations
- University of Wisconsin–Madison