Efficient symbolic analysis of programs
type: Item
instance of: scholarly article
title: Efficient symbolic analysis of programs
zbMATH Open document ID: 0603.68012
DOI: 10.1016/0022-0000(86)90031-0
author: J. Reif
author: Harry R. Lewis
published in: Journal of Computer and System Sciences
publication date: 1986-01-01T00:00:00Z
review text: This paper is concerned with constructing, for each expression in a given program text, a symbolic expression whose value is equal to the value of the text expression for all executions of the program. A cover is a mapping from text expressions to such symbolic expressions. Covers can be used for constant propagation, code motion, and a variety of other program optimizations. Covers can also be used as an aid in symbolic program execution and for finding loop invariants for program verification. We describe a direct (non-iterative) algorithm for computing a cover. The cover computed by our algorithm is characterized as a minimum of a certain fixed point equation, and is in general a better cover than might be computed by iteration methods (which can compute fixed point covers which are not minimal). Our algorithm is efficient and applicable to all flow graphs. A variant of our algorithm is implemented by \textit{R. N. Kalman} and \textit{A. A. Kortesoja} [IEEE Trans. Software Eng. SE-6, 512-519 (1980)] in an optimizing compiler.
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 3974261
zbMATH Keywords: symbolic expression
zbMATH Keywords: text expression
zbMATH Keywords: constant propagation
zbMATH Keywords: code motion
zbMATH Keywords: program optimizations
zbMATH Keywords: loop invariants
zbMATH Keywords: program verification
zbMATH Keywords: cover
zbMATH Keywords: fixed point
zbMATH Keywords: flow graphs
zbMATH Keywords: optimizing compiler
MaRDI profile type: Publication
full work available at URL: 0022-0000(86)90031-0
OpenAlex ID: W2023850308
cites work: Q4068115
cites work: The theory of languages
cites work: Symbolic Evaluation and the Analysis of Programs
cites work: Some Topics in Code Optimization
cites work: Q4162641
cites work: Q4162449
cites work: Q4114748
cites work: Flow Graph Reducibility
cites work: A Simple Algorithm for Global Data Flow Analysis Problems
cites work: Global Data Flow Analysis and Iterative Algorithms
cites work: Monotone data flow analysis frameworks
cites work: Logical analysis of programs
cites work: Q4068060
cites work: Q5670164
cites work: Symbolic execution and program testing
cites work: Q5585020
cites work: A fast algorithm for finding dominators in a flowgraph
cites work: Program Improvement by Source-to-Source Transformation
cites work: Q5613949
cites work: Q3922128
cites work: Efficient approximate solution of sparse linear systems
cites work: Code Motion
cites work: Symbolic Program Analysis in Almost-Linear Time
cites work: Optimization of very high level languages—I
cites work: Depth-First Search and Linear Graph Algorithms
cites work: Fast algorithms for the elimination of common subexpressions
cites work: The synthesis of loop predicates
description: scientific article; zbMATH DE number 3974261