一个出具证明编译器后端的设计与实现

作     者：田波 陈意云 王伟 李兆鹏 王志芳 TIAN Bo;CHEN Yi-yun;WANG Wei;LI Zhao-peng;WANG Zhi-fang

作者机构：中国科学技术大学计算机科学技术系合肥230027 中国科学技术大学苏州研究院软件安全实验室苏州215123 

基　　金：国家自然科学基金资助项目(60673126 90718026) Intel中国研究中心基金资助项目 

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2009年第35卷第7期

页      码：132-135页

摘      要：设计并实现一个类C语言PointerC的出具证明编译器后端。该后端采用最强后条件演算同步处理整型断言和指针断言实现整型验证条件和指针验证条件的证明,能够完全自动地产生目标级程序的指针安全性证明,处理常见递归数据结构中的非一致性别名问题。后端包括独立的定理检查器,能够检验携证明代码的完整性。

主 题 词：高可信软件 出具证明编译器 指针安全 汇编代码 

学科分类：0711[理学-心理学类] 07[理学] 071102[071102] 

核心收录：

D　O　I：10.3969/j.issn.1000-3428.2009.07.045

馆 藏 号：203124040...