×

Systematic design of program transformation frameworks by abstract interpretation. (English) Zbl 1323.68356

Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’02, Portland, OR, USA, January 16–18, 2002. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-450-9). 178-190 (2002).

MSC:

68Q55 Semantics in the theory of computing
68N15 Theory of programming languages
68N20 Theory of compilers and interpreters
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

CVT
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] C.Consel and C.Danvy.Tutorial notes on partial evaluation.20 th POPL ,493 -501,1993,ACM Press. 10.1145/158511.158707
[2] C.ConselandS.Khoo.On-line and off-line partial evaluation:Semantics specifications and correctness proofs.J. Func.Prog.,5(4):461 -500,1995. · Zbl 0846.68062
[3] P.Cousot.Constructive design of a hierarchy of semantics of atransition system by abstract interpretation.ENTCS ,6,25 p.,1997.http://www.elsevier.nl/locate/entcs/volume6. html .
[4] P.Cousot and R.Cousot.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of .xpoints.4 th POPL ,238 -252,1977, ACM Press. 10.1145/512950.512973
[5] P.Cousot and R.Cousot.Static determination of dynamic properties of recursive procedures.IFIP Conf.on Formal Description of Programming Concepts ,237 -277,1977, North-Holland. · Zbl 0393.68080
[6] P.Cousot and R.Cousot.Systematic design of program analysis frameworks.6 th POPL ,269 -282,1979,ACM Press. 10.1145/567752.567778
[7] P.Cousot and R.Cousot.Comparing the Galois connection and widening/narrowing approaches to abstract interpretation.PLILP ’92 ,LNCS 631,269 -295,1992,Springer.
[8] P.Cousot and R.Cousot.A case study in abstract interpretation based program transformation:Blocking command elimination.ENTCS ,45,2001.http://www.elsevier.nl/ locate/entcs/volume45.html ,23p. · Zbl 1260.68089
[9] L.de Alfaro and Z.Manna.Temporal verification by diagram transformations.CAV ’96 ,LNCS 1102,288 -299,1996, Springer.
[10] U.Erlingsson and F.Schneider.SASI enforcement of security policies:a retrospective.NSPW ’99 ,87 -95,1999,ACM Press. 10.1145/335169.335201
[11] N.Halbwachs,F.Lagnier,and P.Raymond.Synchronous observers and the veri .cation of reactive systems. AMAST ’93 ,Workshops in Comp.,83 -96,1994,Springer.
[12] G.Jin,Z.Li,and F.Chen.A theoretical foundation for program transformations to reduce cache thrashing due to true data sharing.Theoret.Comput.Sci.,255(1 -2):449 -481, 2001. 10.1016/S0304-3975(99)00313-8 · Zbl 0973.68254
[13] N.Jones.Abstract interpretation and partial evaluation in functional and logic programming.ISLP ’94 ,17 -22,1994, MIT Press.
[14] N.Jones.An introduction to partial evaluation.ACM Comput.Surv.,28(3):480 -504,1996. 10.1145/243439.243447
[15] N.Jones.Combining abstract interpretation and partial evaluation (brief overview).SAS ’97 ,LNCS 1302,396 -405, 1997,Springer.
[16] N.Jones,C.Gomard,and P.Sestoft.Partial Evaluation and Automatic Program Generation. Prentice-Hall,1993. · Zbl 0875.68290
[17] N.Jones and A.Mycroft.Data flow analysis of applicative programs using minimal function graphs:abridged version. 13 th POPL ,296 -306,1986,ACM Press. 10.1145/512644.512672
[18] G.Kildall.A unified approach to global program optimization.1 st POPL ,194 -206,1973,ACMpress. 10.1145/512927.512945
[19] D.Monniaux.Abstract interpretation of probabilistic semantics.SAS ’2000 ,LNCS 1824,322 -339,2000,Springer. · Zbl 0966.68111
[20] R.Paige.Symbolic finite differencing -part I.ESOP ’90 , LNCS 432,36 -56,1990,Springer. · Zbl 0766.68068
[21] R.Paige.Future directions in program transformations. ACM SIGPLAN Not.,32(1):94 -97,1997. 10.1145/251595.251609
[22] A.Pnueli,O.Shtrichman,andM.Siegel.The code validation tool CVT:Automatic veri .cation of a compilation process.STTT ,2(2):192 -201,1998. · Zbl 1022.68733
[23] J.Reynolds.The discoveries of continuations.Lisp and Symbolic Computation ,6(3/4):233 -248,1993. 10.1007/BF01019459
[24] D.Sands.Proving the correctness of recursion-based automatic program transformations.Theoret.Comput.Sci., 167(1 -2):193 -233,1996. 10.1016/0304-3975(96)00074-6 · Zbl 0874.68025
[25] F.Schneider.Enforceable security policies.TISSEC , 3(1):30 -50,2000. 10.1145/353323.353382
[26] P.Steckler and M.Wand.Selective thunkification.SAS ’94 , LNCS 864,162 -178.Springer,1994.
[27] M.Vardi and P.Wolper.Automata-theoretic techniques for modal logics of programs.J.Comput.System Sci., 32(2):183 -221,1986. 10.1016/0022-0000(86)90026-7 · Zbl 0622.03017
[28] F.Vedrine.Binding-time analysis and strictness analysis by abstract interpretation.SAS ’95 ,LNCS 983,400 -417,1995, Springer.
[29] P.Wadler.Deforestation:Transforming programs to eliminate trees.Theoret.Comput.Sci.,73(2):231 -248,1990. 10.1016/0304-3975(90)90147-A · Zbl 0701.68013
[30] M.Weiser.Program slicing.IEEE Trans.Software Engrg., SE-10(4):352 -357,1984. · Zbl 0552.68004
[31] H.Yang and Y.Sun.Reverse engineering and reusing Cobol programs:A program transformation approach.IWFM ’97 , Electronic Workshops in Computing,1997.http://ewic. org.uk/ewic/workshop/view.cfm/IWFM-97.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.