steve@titan.tsd.arlut.utexas.edu (Steve Glicker) (12/05/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. - - - - - - - Reply-To: Jerry Freedman, Jr., <jfjr@mbunix.mitre.org> (and) H. LUDWIG HAUSEN, <HAUSEN%DBNGMD21.BITNET@CUNYVM.CUNY.EDU> Noted researchers in symbolic evaluation, Thomas E. Cheatham, Jr., 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. - - - - - - - Reply-To: 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. - - - - - - - Reply-To: 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 references, 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) -- Send compilers articles to compilers@iecc.cambridge.ma.us or {ima | spdcc | world}!iecc!compilers. Meta-mail to compilers-request.