Symbolic program analysis in almost linear time


Conference Paper

© 1986 ACM. A global flow model is assumed; as usual, the flow of control is represented by a digraph called the control flow graph. The objective of our program analysis is the construction of a mapping (a cover) from program text expressions to symbolic expressions for their value holding over all executions of the program. The particular cover constructed by our methods is in general weaker than the covers obtainable by the methods of [Ki, FKU, R1], but our method has the advantage of being very efficient; requiring 0(ℓ + aα(a)) extended bit vector operations (a logical operation or a shift to the first nonzero bit) on all control flow graphs (whether reducible or not), where a is the number of edges of the control flow graph, ℓ is the length of the text of the program, and α is Tarjan's function (an extremely slowly growing function).

Full Text

Duke Authors

Cited Authors

  • Reif, JH

Published Date

  • January 1, 1978

Published In

Start / End Page

  • 76 - 83

International Standard Serial Number (ISSN)

  • 0730-8566

Digital Object Identifier (DOI)

  • 10.1145/512760.512769

Citation Source

  • Scopus