SYMBOLIC EVALUATION AND THE ANALYSIS OF PROGRAMS

被引：39
作者：
CHEATHAM, TE
HOLLOWAY, GH
TOWNLEY, JA
机构：
[1] Center for Research in Computing Technology, Harvard University, Cambridge
来源：
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1979年 / 5卷 / 04期
关键词：
Automatic program analysis; expression simplification; first-order recurrence relations; program optimization; program verification; symbolic evaluation;
D O I：
10.1109/TSE.1979.234207
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Symbolic evaluation is a form of static program analysis in which symbolic expressions are used to denote the values of program variables and computations. It does not require the user to specify which path at a conditional branch to follow nor how many cycles of a loop to consider. Instead, a symbolic evaluator uses conditional expressions to represent the uncertainty that arises from branching and develops and attempts to solve recurrence relations that describe the behavior of loop variables. We describe a symbolic evaluator for part of the ELI language [23], with particular emphasis on techniques for handling conditional data sharing patterns, the behavior of array variables, and the behavior of variables in loops and during procedure calls. An expression simplifier, which is the heart of the system, is described in some detail. Potential applications of the symbolic evaluator to problems in program validation, verification, and optimization are mentioned. Copyright © 1979 by The Institute of Electrical and Electronics Engineers, Inc.
引用
收藏
页码：402 / 417
页数：16
相关论文
共 34 条
[1]  
Boyer R.S., Elspas B., Levitt K.N., SELECT-A formal system for testing and debugging programs by symbolic execution, Proc. Int. Conf. on Reliable Software, pp. 21-23, (1975)
[2]  
Cheatham T.E., Townley J.A., Symbolic evaluation of programs-A look at loop analysis, Proc. ACM Symp. Symbolic and Algebraic Computation, pp. 90-96, (1976)
[3]  
Cheatham T.E., Washington D.B., Program loop analysis by solving first order recurrence relations, (1978)
[4]  
Cheatham T.E., Semantic models for programming languages, (1978)
[5]  
Clarke L.A., A system to generate test data and symbolically execute programs, IEEE Trans. Software Eng., SE-2, pp. 215-222, (1976)
[6]  
Conrad W.R., Rewrite user's guide, (1976)
[7]  
COST user's guide
[8]  
PROBE user's guide
[9]  
Deutsch L.P., An interactive program verifier, (1973)
[10]  
Elspas B., The semiautomatic generation of inductive assertions for proving program correctness, (1974)
1234