[1] Lacey D'Jones ND,Wyk EV,Frederiksen CC.Compiler optimization correctness by temporal logic[J].Higher-Order and Symbolic Computation,2004,17(3):173-206. [2] Frederiksen CC.Correctness of classical compiler optimizations using CTL[J].Electronic Notes in Theoretical Computer Science,2002,65(2):37-51. [3] Abo AV,Sethi R,Ullman JD.Compilers:Principles,Techniques,and Tools[M].Boston:Addison-Wesley,1986:86-99. [4] Kozen D,Patron M.Certification of compiler optimizatious using Kleene algebra with tests .In:Lloyd nE Dahl v,Furbach U.Kerber M,Lau K,Palamidessi C.Pereim LM,Sagiv Y,Stuckey PJ,eds.Proc.of the I st Int'l Conf.on Computational Logic(CL2000) .London:Springer-Verlag,2000.568-582. [5] Benton N.Simple relational correctness proofs for static analyses and program transformations[J].ACM SIGPLAN Notices,2004.39(1):14-25. [6] Muchnick SS.Advanced Compiler Design and Implementation[M].San Francisco:Morgan Kaufrnann Publishers,1997:106-110. [7] Alien R,Kennedy K.Optimizing Compilers for Modem Architectures:A Dependence-Based Approach[M].San Francisco:Morgan Kaufinann Publishers,2002:23-30. [8] Wand M.Specifying the correctness of binding time analysis .In:Deusen MV,Lang B,eds.Proc.of the 20th ACM SIGPLANSIGACT Symp.on Principles of Programming Languages .New York:ACM Press,1993.137-143. [9] Wand M,Siveroni I.Constraint systems for useless variable elimination .In:Appel A,Aiken A .eds.Proc.of the 26th ACM SIGPLAN-SlGACT Symp.On Principles of Programming Languages .NewYork:ACMPress,1999.291-302. [10] Kubayashi N.Type-Based useless variable elimination [J].ACM S1GPLANNotices,1999,34(11):84-93. [11] Kozen,D Efficient code certification.Technical Report .Cornell Univer-sity,Ithaca,USA,1998:98-166. [12] Morrisett G,Walker D,Crary K,Glew N.From system F to typed assem-bly language .ACM Transactions on Programming Languages and Systems .Tennessee,USA,1999,21(3):527-568. [13] Necula,G.Proof-carrying code .In:Proc of the 24th ACM SIGPLAN-SIGACT SYMP .On Principles of Programming Languages,New York,USA,1997.106-119. [14] 胡定磊,陈书明.基于互补谓词的编译优化[J].电子学报,2006,34(07):1280-1285. HU Ding-lei,CHEN Shu-ming.Optimizing compiler based on complementary predicate[J].Acta Electronica Sinica,2006,34(07):1280-1285.(in Chinese) [15] 胡定磊,陈书明.低功耗编译技术综述[J].电子学报,2005,33(04):676-681. HU Ding-lei,CHEN Shu-ming.Low power/ energy compilation technology[J].Acta Electronica Sinica,2005,33(04):676-681.(in Chinese) [16] 唐遇星,邓,周兴铭.基于Trace-Cache的多级动态优化框架设计[J].电子学报,2005,33(11):1946-1951. TANG Yu-xing,DENG Kun,ZHOU Xing-ming.Trace-cache based framework for mult-i level dynamic optimization[J].Acta Electronica Sinica,2005,33(11):1946-1951.(in Chinese) [17] PC Van Oorschot.Revisiting software protection .In:Proc of 6th international Information Security Conference (ISC'03).Lecture Notes in Computer Science 2851 .Berlin:Springer-Verlag,2006.1-13. [18] A Appel.Verified software toolchain[J].Programming Languages and Systems,2011,66(02):1-17. [19] 何炎祥,吴伟,刘陶,等.可信编译理论及其核心实现技术[J].计算机科学与探索,2011,5(1):1-22. HE Yanxiang,WU Wei,LIU Tao.Theory and key implementation techniques of trusted compiler:A survey[J].Journal of Frontiers of Computer Science and Technology,2011,5(1):1-22.(in Chinese) [20] X Yang,Y Chen,E Eide,J Regehr.Finding and understanding bugs in C compilers .In 32nd Conf.on Programming Language Design and Implementation (PLDI'11) .San Jose,California,2011.283-294. [21] S Kundu,Z Tatlock,S Lerner.Proving optimizations correct using parameterized program equivalence[J].ACM Sigplan Notices,2009,44(6):327-337. [22] Lerner S,Millstein T,Chambers C.Automatically proving the correctlless of compiler optimizations[J].ACM SIGPLAN Notices,2003,38(5):220-231. [23] Necula GC.Translation validation for optimizing compiler[J].Acm Sigplan Notices,2000.35(5):83-94. [24] Zaks A,Pnueli A.Program analysis for compiler validation .In:Proc.of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering .New York,USA,2008.1-7. [25] 聂久焘,程旭,王克义.一种高效的完全值编号算法[J].电子学报,2010,38(2):416-421. NIE Jiu-tao,CHENG Xu,WANG Ke-yi.An efficient complete global value numbering algorithm[J].Acta Electronica Sinica,2010,38(2):416-421.(in Chinese) |