Accession Number : ADA326038

Title :   Semantics-based Program Analysis via Symbolic Composition of Transfer Relations.

Descriptive Note : Doctoral thesis,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Colby, Christopher

PDF Url : ADA326038

Report Date : 16 AUG 1996

Pagination or Media Count : 177

Abstract : The goal of program analysis is to determine automatically properties of the run-time behavior of a program. Tools of software development such as compilers program verification systems and program-comprehension systems are in large part based on program analyses. Most semantics-based program analyses model the run-time behavior of a program as a trace of execution states and compute a property of these states. Typically this property is drawn from a predetermined language of semantic information such as aliasing descriptions or types of values. The standard methodology of program analysis is to construct the property as a fixed point a single execution step at a time. We explain that these ubiquitous methodological choices--the a priori choice of the describable program properties and the use of a fixed-point computation-have some fundamental limitations and can result in poor precision. In this dissertation we present a different approach to semantics-based program analysis. Our methodology is based on transfer relations that precisely describe the changes between the state of memory one point during execution and the state of memory at some later point in the execution. We isolate a language TR of concise computer-representable presentations of transfer relations. We also give an algorithm that given two transfer relations from TR symbolically constructs a third transfer relation in TR that is semantically equivalent to their relational composition. An analysis designer begins by describing the operational semantics of a source language as a set of TR-terms that precisely describe the atomic steps of execution. Then an analysis algorithm repeatedly applies to build a precise run-time description of any finite control path of interest.

Descriptors :   *COMPUTER PROGRAM DOCUMENTATION, *ALGORITHMS, *PROGRAMMING LANGUAGES, *COMPILERS, *DEBUGGING(COMPUTERS), SEMANTICS, THESES, TIME, STANDARDIZATION, COMPUTER PROGRAM VERIFICATION.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE