Computer Science ›› 2014, Vol. 41 ›› Issue (Z6): 334-338.
Previous Articles Next Articles
LIU Yang,YANG Fei,SHI Gang,YAN Xin,WANG Sheng-yuan and DONG Yuan
| [1] Necula G C．Proof-Carrying Code[C]∥POPL’97．ACM press,1997:106-119 [2] Cimatti A,Giunchiglia F,Pecchiari P,et al.A Provably Correct Embedded Verifier for the Certification of Safety Critical Software[C]∥Grumberg O,ed．Proc．9th Intl．Conference on Computer Aided Verification (CA V’97)．Lect．Notes in Comp．Sci.,Springer-Verlag,1997,1254:202-213 [3] Pnueli A,Siegel M,Singerman E．Translation Validation[C]∥Proc．4th Intl．Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98)．1998:151-166 [4] Pnueli A,Shtrichman O,Siegel M．Translation Validation forSynchronous Languages[C]∥Larsen K G,Skyum S,Winskel G,eds.ICALP 1998．LNCS． Heidelberg:Springer,1998:1443:235-246 [5] Pnueli A,Singerman E,Siegel M．Translation Validation:from SIGNAL to C[C]∥Volume 1710of LNCS State-of-the-Art Survey．Springer-Verlag,1999:231-255 [6] Pnueli A,Shtrichman O,Siegel M．Translation validation:FromDC+ to C[C]∥Proceedings of the International Workshop on Current Trends in Applied Formal Method:Applied Formal Methods．Volume 1641of Lect．Notes in Comp.Sci.,1998:137-150 [7] Pnueli A,Siegel M,Shtrichman O．The code validation tool(CVT)-automatic verification of a compilation process[J]．Int．Journal of Software Tools for Technology Transfer (STTT),1999,2(2):192-201 [8] Necula G C．Translation validation for an optimizing compiler[C]∥Programming Language Design and Implementation 2000．ACM Press,2000:83-95 [9] Zuck L,Pnueli A,Leviathan R．Validations of optimizing compliers[R]．Weizmann Institute of Science,2000 [10] Zuck L,Pnueli A,Fang Y,et al．Voc:A methodology for thetranslation validation of optimizing compilers[J]．Jounal of Universal Computer Science,2003,9(3):223-247 [11] Zuck L,Pnueli A,Fang Y,et al．Translation and Run-Time Validation of Optimized Code[C]∥Electronic Notes in Theoretical Computer Science．2002 [12] Zuck L,Pnueli A,Goldberg B,et al．Translation and run-time validation of loop transformations[C]∥Proceedings of the Run-Time Result Verification Workshop,Electronic Notes in Theoretical Computer Science (ENTCS)．volume 70,2002 [13] Ryabtsev M,Strichman O．Translation validation:From Simulink to C[M]∥Computer Aided Verification．Springer,2009 [14] Rival X．Symbolic transfer function-based approaches to certified compilation[C]∥31st symposium Principles of Programming Languages．ACM Press,2004:1-13 [15] Tristan J-B,Leroy X．Formal verification of translation validators:A case study on instruction scheduling optimizations[C]∥35th symposium Principles of Programming Languages．ACM Press,2008:17-27 [16] Tristan J-B,Leroy X．Verified Validation of Lazy Code Motion[C]∥Programming Language Design and Implementation 2009．ACM Press,2009:316-326 [17] Tate R,Stepp M,Tatlock Z,et al.Equality saturation:A new approach to optimization[C]∥36th Principles of Programming Languages．ACM,2009:264-276 [18] Tristan J-B,Leroy X．Evaluating Value-Graph Translation Validation for LLVM[C]∥32nd ACM SIGPLAN conference on Programming language design and implementation．ACM Press,2011:295-305 [19] Tristan J-B,Leroy X．A Simple,Verified Validator for Software Pipelining[C]∥37th symposium Principles of Programming Languages．ACM Press,2010:83-92 [20] Tristan J-B．Formal verification of translation validators[D]．Universite Paris-Diderot-Paris VII,2009 [21] Huang Yu-qiang,Childers B R, Soffa M L．Catching and identifying bugs in register allocation[C]∥Static Analysis,13th Int．Symp.,SAS 2006．volume 4134of Lecture Notes in Computer Science．Springer,2006:281-300 [22] Kanade A,Sanyal A,Khedker U．A PVS based framework for validating compiler optimizations[C]∥SEFM’06:Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods．IEEE Computer Society,2006:108-117 [23] Colby C,Lee P,Necula G C,et al.A certifying compiler for Java[J]．ACM SIGPLAN Notices,2000,35(5):95-107 [24] Chirica L M,Martin D F．An approach to compiler correctness[J]．ACM SIGPLAN Notices,1975,10(6):96-103 [25] Ngo V C,Talpin J-P,Gautier T,et al．Formal Verification ofSynchronous Data-flow Compilers[R]．Project-Team ESPRESSO Research Report,March 2012:7921 [26] Rinard M,Marinov D．Credible compilation with pointers[C]∥Workshop on Run-Time Result Verification．1999 [27] Barret C W,Fang Yi,Goldberg B,et al．TVOC:A translationvalidator for optimizing compilers[C]∥Computer Aided Verification,17th Int．Conf.,CAV 2005．volume 3576of Lecture Notes in Computer Science．Springer,2005:291-295 [28] Zaks A,Pnueli A．Covac:Compiler validation by program analysis of the cross-product[C]∥FM 2008:Formal Methods,15th International Symposium on Formal Methods．volume 5014of Lecture Notes in Computer Science．Springer,2008: 35-51 [29] Leroy X．Formal verification of a realistic compiler[M]∥Communications of the ACM,2009 [30] Leroy X．The Compcert verified compiler,software and commented proof．http://compcert.inria.fr/,Jan．2010 [31] Fang Yi．Translation Validation of Optimizing Compilers[D]．New York University,2005 [32] Goldberg B,Zuck L,Barret C．Into the loops:Practical issues in translation validation for optimizing compilers[C]∥Proc.Workshop Compiler Optimization Meets Compiler Verification (COCV 2004)．volume 132of Electronic Notes in Theoretical Computer Science．Elsevier,2005:53-71 [33] Pnueli A,Zaks A．Translation validation of interprocedural optimizations[C]∥Proceedings of the 4th International Workshop on Software Verification and Validation(SVV)．2006 [34] Stepp M,Tate R,Lerner S．Equality-Based translation validator for LLVM[C]∥CAV’11:Proceedings of the 23rd International Conference on Computer Aided Verification．2011 [35] Barthe G,Demange D,Pichardie D．A formally verified SSA-based middle-end-Static Single Assignment meets CompCert[C]∥ESOP’12．2012 [36] 何炎祥,刘陶,吴伟．可信编译器关键技术研究[J]．计算机工程与科学,2010,32(8):1-6 |
| No related articles found! |
|
||
Home