Patrick Cousot
Radhia Cousot
ABSTRACT
We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixpoint trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.
- 1.C.Consel and C.Danvy.Tutorial notes on partial evaluation.20 th POPL ,493 -501,1993,ACM Press. Google Scholar
Digital Library
- 2.C.ConselandS.Khoo.On-line and off-line partial evaluation:Semantics specifications and correctness proofs.J. Func.Prog.,5(4):461 -500,1995.Google ScholarCross Ref
- 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 .Google Scholar
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 6.P.Cousot and R.Cousot.Systematic design of program analysis frameworks.6 th POPL ,269 -282,1979,ACM Press. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 9.L.de Alfaro and Z.Manna.Temporal verification by diagram transformations.CAV '96 ,LNCS 1102,288 -299,1996, Springer. Google ScholarDigital Library
- 10.U.Erlingsson and F.Schneider.SASI enforcement of security policies:a retrospective.NSPW '99 ,87 -95,1999,ACM Press. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 13.N.Jones.Abstract interpretation and partial evaluation in functional and logic programming.ISLP '94 ,17 -22,1994, MIT Press. Google ScholarDigital Library
- 14.N.Jones.An introduction to partial evaluation.ACM Comput.Surv.,28(3):480 -504,1996. Google ScholarDigital Library
- 15.N.Jones.Combining abstract interpretation and partial evaluation (brief overview).SAS '97 ,LNCS 1302,396 -405, 1997,Springer. Google ScholarDigital Library
- 16.N.Jones,C.Gomard,and P.Sestoft.Partial Evaluation and Automatic Program Generation. Prentice-Hall,1993. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 18.G.Kildall.A unified approach to global program optimization.1 st POPL ,194 -206,1973,ACMpress. Google ScholarDigital Library
- 19.D.Monniaux.Abstract interpretation of probabilistic semantics.SAS '2000 ,LNCS 1824,322 -339,2000,Springer. Google ScholarDigital Library
- 20.R.Paige.Symbolic finite differencing -part I.ESOP '90 , LNCS 432,36 -56,1990,Springer. Google ScholarDigital Library
- 21.R.Paige.Future directions in program transformations. ACM SIGPLAN Not.,32(1):94 -97,1997. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 23.J.Reynolds.The discoveries of continuations.Lisp and Symbolic Computation ,6(3/4):233 -248,1993. Google ScholarDigital Library
- 24.D.Sands.Proving the correctness of recursion-based automatic program transformations.Theoret.Comput.Sci., 167(1 -2):193 -233,1996. Google ScholarDigital Library
- 25.F.Schneider.Enforceable security policies.TISSEC , 3(1):30 -50,2000. Google ScholarDigital Library
- 26.P.Steckler and M.Wand.Selective thunkification.SAS '94 , LNCS 864,162 -178.Springer,1994.Google Scholar
- 27.M.Vardi and P.Wolper.Automata-theoretic techniques for modal logics of programs.J.Comput.System Sci., 32(2):183 -221,1986. Google ScholarDigital Library
- 28.F.Vedrine.Binding-time analysis and strictness analysis by abstract interpretation.SAS '95 ,LNCS 983,400 -417,1995, Springer. Google ScholarDigital Library
- 29.P.Wadler.Deforestation:Transforming programs to eliminate trees.Theoret.Comput.Sci.,73(2):231 -248,1990. Google ScholarDigital Library
- 30.M.Weiser.Program slicing.IEEE Trans.Software Engrg., SE-10(4):352 -357,1984.Google ScholarDigital Library
- 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.Google Scholar
- Systematic design of program transformation frameworks by abstract interpretation
Recommendations
Systematic design of program transformation frameworks by abstract interpretation
We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed ...
Proving Theorems by Program Transformation
To Andrzej Skowron on His 70th BirthdayIn this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming ...
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural ...
Comments