steve@titan.tsd.arlut.utexas.edu (Steve Glicker) (11/28/90)
I am looking for literature on symbolic evalution methods for program analysis. I have "PROGRAM FLOW ANALYSIS: Theory and Applications," edited by Steven S. Muchnick and Neil D. Jones, 1981 but I'm very interested in more recent material. References to literature which is application-oriented would be most helpful, but any applicable references would be appreciated. Please email responses directly to me. -- Steve Glicker Applied Research Laboratories The University of Texas at Austin (steve@titan.tsd.arlut.utexas.edu)
steve@titan.tsd.arlut.utexas.edu (Steve Glicker) (12/06/90)
Several people have expressed interest in the results of the inquiry
on symbolic evaluation methods. I have provided them below in a
condensed form. I apologize for any transcription errors or
misrepresentations.
- - - - - - -
From: Jerry Freedman, Jr., <jfjr@mbunix.mitre.org>
(and)
H. LUDWIG HAUSEN, <HAUSEN%DBNGMD21.BITNET@CUNYVM.CUNY.EDU>
Noted researchers in symbolic evaluation,
Cheatham, Harvard (late seventies)
Lori Clarke, Umass Amherst
E. Ploedereder, Harvard or Tratran Labs
Also see some Testing conferences (Bannf Meetings). Ask L. Clarke for
more.
- - - - - - -
From: Paul Havlak <paco@rice.edu>
I'm doing a thesis on what I call "symbolic analysis" -- techniques for the
representation and comparison of expressions that are not known to be constant.
There are three basic approaches:
Determining equality of expressions by value numbering
@Article{ReLe:Symbolic,
Author={J. H. Reif and H. R. Lewis},
Title={Symbolic evaluation and the global value graph},
Journal=POPL77,
Pages={104-118},
Month=Jan,
Year={1977}}
@InProceedings{Reif:Symbolic, Author={J. H. Reif},
Title={Symbolic Program Analysis in Almost Linear Time},
BookTitle=POPL78, Pages={76-83},
Month=Jan, Year={1978}}
@Article{ReTa:Symbolic,
Author={J. H. Reif and R. E. Tarjan},
Title={Symbolic Program Analysis in Almost-Linear Time},
Journal={SIAM Journal on Computing},
Volume={11},
Number={1},
Pages={81-93},
Month=Feb,
Year={1981}}
There's also Reif & Lewis '82, which I don't have.
@inproceedings{RoWZ:Global,
Author={B. K. Rosen and M. N. Wegman and F. K. Zadeck},
Title={Global Value Numbers and Redundant Computations},
BookTitle=POPL88,
Address={San Diego, CA},
Pages={12-27},
Month=Jan,
Year={1988}}
@inproceedings{AlWZ:Equality,
Author={B. Alpern and M. N. Wegman and F. K. Zadeck},
Title={Detecting Equality of Variables in Programs},
BookTitle=POPL88,
Address={San Diego, CA},
Pages={1-11},
Month=Jan,
Year={1988}}
Propagating linear constraints among variables
@article{Karr:Affine,
author={ M. Karr},
title={ Affine Relationships Among Variables of a Program },
journal={Acta Informatica},
Volume={6},
pages={133-151},
year={1976},
publisher={Springer-Verlag},
ignore={ }}
@inproceedings{CoHa:Automatic,
author={ P. Cousot and N. Halbwachs},
title={ Automatic Discovery of Linear Restraints
Among Variables of a Program },
booktitle=POPL78,
pages={84-96},
year={1978},
ignore={ }}
Expression folding and simplification
This is a less theoretical approach, and hasn't been described
in much detail in the literature. Expression folding (forward
propagation of left-hand sides) is essentially subsumed in power
by value numbering techniques. But value numbering doesn't
work well with expression simplification and cancelling.
This seems to be the preferred approach for current dependence
analyzers, used for vectorization and parallelization.
@Article{AlKe:Automatic,
Author={J. R. Allen and K. Kennedy},
Title={Automatic Translation of {FORTRAN}
Programs to Vector Form},
Journal=TOPLAS, Volume={9}, Number={4},
Pages={491-542}, Month=Oct, Year={1987}}
@phdthesis{Alle:Dissertation,
author={ J. R. Allen},
title={ Dependence Analysis for Subscripted Variables
and its Application to Program Transformation }
year={1983},
month=Apr,
school={Rice University, Dept. of Mathematical Sciences},
ignore={ }}
POPL is the SIGPLAN/SIGACT conference on Principles of Programming
Languages. I don't know if it is also included in any periodical series.
TOPLAS is ACM Transactions on Programming Languages and Systems.
- - - - - - -
From: Irvin Shizgal <Irvin.Shizgal@newcastle.ac.uk>
Not surprisingly there's a lot of work on symbolic evaluation of
Prolog (since it's easier to do than most conventional languages.)
I know that Bruynooge et al at the University of Leuven (Belgium)
have done quite a bit of work in this area.
- - - - - - -
In addition, I've come across the following,
Clarke, L.A.; Richardson, D.J. (1985). "Applications of symbolic
evaluation," Journal of Systems and Software, vol. 5, no. 1, 15-35
Ploedereder, Erhard. "Symbolic evaluation as a basis for integrated
validation," Inspection-testing-verification-alternatives.Proc. of a
symposium (Darmstadt, West Germany, Sept. 25-30, 1983), H. Hausen
(Ed.), Elsevier North-Holland, Inc., New York, NY, 1984, 167--185.
--
Steve Glicker
Applied Research Laboratories
The University of Texas at Austin
(steve@titan.tsd.arlut.utexas.edu)