References: |
[Ake78] Sheldon B. Akers. Binary decision diagrams. IEEE Transactions on Computers, 27(6):509–516, June 1978. [ALSU07] Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Pearson Education;, 2nd edition edition, 2007. [App98] A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998. [Ass96] U. Assmann. How to uniformly specify program analysis and transformation with graph rewrite systems. In P. Fritzson, editor, Compiler Construction 1996, volume 1060 of Lecture Notes in Computer Science. Springer, 1996. [Ass99] Uwe Assmann. OPTIMIX, A Tool for Rewriting and Optimizing Programs. In Graph Grammar Handbook, Vol. II. Chapman-Hall, 1999. [BLQ+03] Marc Berndl, Ondrej Lhot´ak, Feng Qian, Laurie Hendren, and Navindra Umanee. Points-to analysis using bdds. In PLDI ’03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pages 103–114, New York, NY, USA, 2003. ACM. [Boy70] J. M. Boyle. A transformational component for programming languages grammar. Technical Report ANL-7690, Argonne National Laboratory, IL, 1970. [Boy89] J. M. Boyle. Abstract programming and program transformation. In Software Reusability Volume 1, pages 361–413. Addison-Wesley, 1989. [Bry86] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEE Transactions on Computers C-35, 12:1035–1044, December 1986. [CCH95] J. R. Cordy, I. H. Carmichael, and R. Halliday. The TXL programming language, version 8. Legasys Corporation, April 1995. [CES96] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8:244–263, 1996. [CS92] R. Cleaveland and B. Steffen. A linear–time model–checking algorithm for the alternation–free modal mu–calculus. In Kim G. Larsen and Arne Skou, editors, Proceedings of Computer Aided Verification (CAV ’91), volume 575, pages 48–58, Berlin, Germany, 1992. Springer. [dMDLS03] Oege de Moor, Stephen Drape, David Lacey, and Ganesh Sittampalam. Incremental program analysis via language factors. Program Tools Group, Oxford., 2003. [dMS01] Oege de Moor and Ganesh Sittampalam. Higher-order matching for program transformation. Theoretical Computer Science, 269(1- 2):135–162, October 2001. [DRW96] Steven Dawson, C. R. Ramakrishnan, and David S. Warren. Practical program analysis using general purpose logic programming systems — A case study. ACM SIGPLAN Notices, 31(5):117–126, May 1996. [FH91] C. W. Fraser and D. R. Hanson. A retargetable compiler for ANSI C. Technical Report CS–TR–303–91, Princeton, N.J., 1991. [FNP97] R. E. Faith, L. S. Nyland, and J. F. Prins. KHEPERA: A system for rapid implementation of domain-specific languages. In Proceedings USENIX Conference on Domain-Specific Languages, pages 243–255, 1997. [Hec88] R. Heckmann. A functional language for the specification of complex tree transformations. In ESOP ’88, Lecture Notes in Computer Science, pages 175–190. Springer-Verlag, 1988. [JTH01] Simon Peyton Jones, Andrew Tolmach, and Tony Hoare. Playing by the rules: Rewriting as a practical optimisation technique in ghc. In Proceedings of the 2001 Haskell Workshop, pages 203–233, September 2001. [KKKS96] M. Klein, D. Knoop, D. Koschutzki, and B. Steffen. DFA & OPTMETAFrame: A toolkit for program analysis and optimization. In Procs. of the 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’96), volume 1055 of Lecture Notes in Computer Science, pages 422–426. Springer, 1996. [Kno98] Jens Knoop. Optimal interprocedural program optimization: A new framework and its application. Number 1428 in LNCS Tutorial. Springer-Verlag, 1998. [Koz83] Dexter Kozen. Results on the proposition mu-calculus. Theoretical Computer Science, 27, 1983. [KRS] J. Knoop, O. Ruthing, and B. Steffen. Lazy strength reduction. [KRS92] J. Knoop, O. Ruething, and B. Steffen. Lazy code motion. In Proceedings of the ACM SIGPLAN ’92 Conference on Programming Language Design and Implementation, volume 27, pages 224–234, San Francisco, CA, June 1992. [KSK06] Aditya Kanade, Amitabha Sanyal, and Uday Khedker. A PVS based framework for validating compiler optimizations. In SEFM ’06: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, pages 108–117, Washington, DC, USA, 2006. IEEE Computer Society. [KSK07] Aditya Kanade, Amitabha Sanyal, and Uday Khedker. Structuring optimizing transformations and proving them sound. ENTCS, 176(3), 2007. Proceedings of the 5th International Workshop on Compiler Optimization meets Compiler Verification (COCV’06). [Lac03] David Lacey. Program Transformation using Temporal Logic Specifications. PhD thesis, Oxford University Computing Laboratory, 2003. [LdM01] D Lacey and O de Moor. Imperative program transformation by rewriting. In R Wilhelm, editor, Compiler Construction, volume 2027 of Lecture Notes in Computer Science, pages 52–68. Springer Verlag, 2001. [LGC02] Sorin Lerner, David Grove, and Craig Chambers. Combining dataflow analyses and transformations. In Conference Record of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), 2002. [LJWF02] David Lacey, Neil Jones, Eric Van Wyk, and Carl Christian Frederikson. Proving the correctness of classical compiler optimisation by temporal logic. In Priniciples of Programming Languages, 2002. [LJWF04] David Lacey, Neil Jones, Eric Van Wyk, and Carl Christian Frederikson. Proving correctness of compiler optimizations by temporal logic. Higher-Order and Symbolic Computation, 17(2), 2004. [LMC03] S. Lerner, T. Millstein, and C. Chambers. Automatically proving the correctness of compiler optimizations, 2003. [LMRC05] Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In POPL ’05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 364–377, New York, NY, USA, 2005. ACM Press. [LMW88] P. Lipps, U. M¨onke, and R. Wilhelm. OPTRAN – a language/ system for the specification of program transformations: system overview and experiences. In Proceedings 2nd Workshop on Compiler Compilers and High Speed Compilation, volume 371 of Lecture Notes in Computer Science, pages 52–65, 1988. [LR91] W. Landi and B. Ryder. Pointer induced aliasing: A problem classification. In ACM Symposium on Principles of Programming Languages, pages 93–103, 1991. [McM93] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. [MOR01] Markus M¨uller-Olm and Oliver R¨uthing. On the complexity of constant propagation. In D. Sands, editor, ESOP, volume 2028 of LNCS. Springer-Verlag, 2001. [Muc97] S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997. [NPW02] Tobias Nipkow, Lawrence C. Paulson, and Marcus Wenzel. Isabelle/ HOL: A Proof Assistant for Higher-order Logic, volume 2283 of LNCS. Springer-Verlag, 2002. [Pai94] R. Paige. Viewing a program transformation system at work. In Proceedings Programming Language Implementation and Logic Programming (PLILP), and Algebraic and Logic Programming (ALP), volume 844 of Lecture Notes in Computer Science, pages 5–24. Springer, 1994. [PS89] Lori L. Pollock and Mary-Lou Soffa. An incremental version of iterative data flow analysis. IEEE Transactions on Software Engineering, 15(12):1537–1549, December 1989. [PW86] David A. Padua and Michael J. Wolfe. Advanced compiler optimizations for supercomputers. Communications of the ACM, 29(12):1184–1201, 1986. [SCK+95] B. Steffen, A. Classen, M. Klein, J. Knoop, and T. Margaria. The fixpoint-analysis machine. In Concurrency Theory, 6th International Conference (CONCUR ’95), volume 962. LNCS, Springer- Verlag, 1995. [SS94] Oleg Sokolsky and Scott Smolka. Incremental model checking in the modal μ-calculus. In David Dill, editor, Computer Aided Verification, volume 818 of LNCS, pages 351–363. Springer-Verlag, 1994. [Ste91] B. Steffen. Data flow analysis as model checking. In Proceedings of Theoretical Aspects of Computer Science, pages 346–364, 1991. [Ste93a] B. Steffen. Generating data flow analysis algorithms from modal specifications. Science of Computer Programming, 21:115–139, 1993. [Ste93b] B. Steffen. Generating data flow analysis algorithms from modal specifications. Science of Computer Programming, 21:115–139, 1993. [Tar73] Robert Tarjan. Testing flow graph reducibility. In STOC ’73: Proceedings of the fifth annual ACM symposium on Theory of computing, pages 96–107, New York, NY, USA, 1973. ACM. [TH92] Steven W. K. Tjiang and John L. Hennessy. Sharlit: a tool for building optimizers. SIGPLAN Not., 27(7):82–93, 1992. [VBT98] E. Visser, Z. Benaissa, and A. Tolmach. Building program optimizers with rewriting strategies. In International Conference on Functional Programming ’98, ACM SigPlan, pages 13–26. ACM Press, 1998. [vE98] Robert van Engelen. Ctadel: A Generator of Efficient Codes. PhD thesis, Leiden University, 1998. [vE01] Robert A. van Engelen. Efficient symbolic analysis for optimizing compilers. In R Wilhelm, editor, Compiler Construction, volume 2027 of Lecture Notes in Computer Science. Springer Verlag, 2001. [VRCG+99] Raja Vall´ee-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. Soot - a java bytecode optimization framework. In CASCON ’99: Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, page 13. IBM Press, 1999. [Whi91] Deborah Whitfield. A Unifying Framework for Optimising Transformations. PhD thesis, University of Pittsburgh, 1991. [WL04] John Whaley and Monica S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. SIGPLAN Not., 39(6):131–144, 2004. [WS97] D. L. Whitfield and M. L. Soffa. An approach for exploring code improving transformations. ACM Transactions on Programming Languages and Systems, 19(6):1053–1084, 1997. [WZ91] Mark N. Wegman and F. Kenneth Zadeck. Constant propagation with conditional branches. ACM Transactions on Programming Languages and Systems (TOPLAS), 13(2):181–210, April 1991. [ZCW+02] Wankang Zhao, Baoshen Cai, David Whalley, Mark W.Bailey, Robert Van Engelen, Xin Yuan, Jason D. Hiser, Jack W. Davidson, Kyle Gallivan, and Douglas L. Jones. Vista: A system for interactive code improvement. In LCTES’02-SCOPES’02. ACM, June 2002. |