期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

一个出具证明编译器原型系统的实现 被引量：1

Implementation of certifying compiler prototype
下载PDF
导出
摘要 出具证明编译器是随着人们对现今的软件提出更高的可靠性和安全性要求而产生的工具,它结合了以往程序设计和程序安全性证明的技术。论文介绍了一个出具证明编译器原型系统的实现。 Certifying compiler is such a tool coming up with the increasing demands for higher reliability and safety of computer software.h combines the techniques in programming languages and program verifications.This paper describes some details in implementing our prototype of a certifying compiler.
作者 刘诚 陈意云 葛琳 华保健
机构地区 中国科学技术大学计算机科学技术系
出处 《计算机工程与应用》 CSCD 北大核心 2007年第21期99-102,114,共5页 Computer Engineering and Applications
基金 国家自然科学基金(the National Natural Science Foundation of China under Grant No.60673126) Intel中国研究中心资助。
关键词 软件安全 出具证明编译器 验证条件 形式化证明方法 证明生成器 software safety certifying compiler verification condition formal proof method proof generator
分类号 TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献9

  • 1Necula G.Compiling with proofs[D].School of Computer Science,Carnegie Mellon Univ,1998.
  • 2Necula G C,Lee P.The design and implementation of a certifying compiler[C]//Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation,1998:333-344.
  • 3Colby C,Lee P,Necula G C,et al.A certifying compiler for Java[C]//Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation,2000:95-107.
  • 4Yu Dachuan,Hamid N A,Shao Zhong.Building certified libraries for PCC:dynamic storage allocation[C]//Proc 2003 European Symposium on Programming(ESOP'03).Warsaw,Poland,2003.
  • 5Feng X,Shao Z,Vaynberg A,et al.Modular verification of assembly code with stack-based control abstractions[C]//Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation,2006:401-414.
  • 6Hoare C A R.An axiomatic basis for computer programming[J].Communications of the ACM,1969,12(10):576-580.
  • 7Bertot Y,Casteran P.Coq'Art:the calculus of inductive constructions[M].Berlin:Springer-Verlag,2004.
  • 8The Coq development team.The Coq Proof Assistant Reference Manual[EB/OL].http://coq.inria.fr/.
  • 9Design of a Certifying Compiler Supporting the Proof of Program Safety[EB/OL].http://ssg.ustcsz.edu.cn/lss/.

同被引文献5

  • 1Chen Yiyun, Ge Lin, Hua Baojian, et al. Design of a Certifying Compiler Supporting Proof of Program Safety[C]//Proc. of TASE'07. [S. l.]: IEEE Press, 2007.
  • 2Chen Yiyun, Ge Lin, Hua Baojian, et al. A Pointer Logic and Certifying Compiler[J]. Frontiers of Computer Science in China, 2007, 1(3): 297-312.
  • 3Cooper D C. Theorem Proving in Arithmetic Without Multiplication[M]//Meltzer B, Michie D. Machine Intelligence, [S. l.]: Edinburgh University Press, 1972.
  • 4Deutsch A. Interprocedural May-alias Analysis for Pointers: Beyond K-limiting[C]//Proc. of PLDF94.[S. l.]: ACM Press, 1994.
  • 5葛琳,陈意云,华保健,李兆鹏,刘诚.汇编代码验证中的形式规范自动生成[J].小型微型计算机系统,2008,29(7):1219-1224. 被引量：3

引证文献1

二级引证文献1

计算机工程与应用
2007年 第21期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部