出具证明编译器中代码优化与程序规范转换

• 作者: 李兆鹏 范大威 蒋信予
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 规范转换 代码优化 数据流分析 出具证明编译器
• 年，卷（期）: 2011,（7）
• 所属期刊栏目: 计算机软件与数据库技术
• 页码范围: 1400-1405
• 分类号: TP311
• 字数: 7469字
• 语种: 中文

摘要

出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李兆鹏	中国科学技术大学计算机科学与技术学院	17	99	7.0	9.0
5	范大威	中国科学技术大学计算机科学与技术学院	1	2	1.0	1.0
9	蒋信予	中国科学技术大学计算机科学与技术学院	2	2	1.0	1.0