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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 16, 1996
Accession Number
ADA326038

Entities

People

  • Christopher Colby

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Algorithms
  • C Programming Language
  • Case Studies
  • Computer Languages
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Debugging
  • Grammars
  • Language
  • Linguistics
  • Lists (Data Structures)
  • Machine Languages
  • Programming Languages
  • Real Numbers
  • Theoretical Computer Science

Fields of Study

  • Computer science
  • Engineering

Readers

  • Artificial Intelligence
  • Software Engineering.
  • Theoretical Analysis.