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.
[3]
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.
[4]
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.
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.
[7]
胡定磊,陈书明.基于互补谓词的编译优化[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)
[8]
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.
[9]
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.
[10]
聂久焘,程旭,王克义.一种高效的完全值编号算法[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)
[11]
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.
[12]
Frederiksen CC.Correctness of classical compiler optimizations using CTL[J].Electronic Notes in Theoretical Computer Science,2002,65(2):37-51.
[13]
Benton N.Simple relational correctness proofs for static analyses and program transformations[J].ACM SIGPLAN Notices,2004.39(1):14-25.
[14]
Muchnick SS.Advanced Compiler Design and Implementation[M].San Francisco:Morgan Kaufrnann Publishers,1997:106-110.
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.
[18]
胡定磊,陈书明.低功耗编译技术综述[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)
[19]
唐遇星,邓,周兴铭.基于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)
[20]
A Appel.Verified software toolchain[J].Programming Languages and Systems,2011,66(02):1-17.
[21]
何炎祥,吴伟,刘陶,等.可信编译理论及其核心实现技术[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)
[22]
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.
[23]
S Kundu,Z Tatlock,S Lerner.Proving optimizations correct using parameterized program equivalence[J].ACM Sigplan Notices,2009,44(6):327-337.
[24]
Lerner S,Millstein T,Chambers C.Automatically proving the correctlless of compiler optimizations[J].ACM SIGPLAN Notices,2003,38(5):220-231.
[25]
Necula GC.Translation validation for optimizing compiler[J].Acm Sigplan Notices,2000.35(5):83-94.
