| 出具证明编译器中代码优化与程序规范转换 |
| |
| 引用本文： | 范大威,李兆鹏,蒋信予.出具证明编译器中代码优化与程序规范转换[J].小型微型计算机系统,2011,32(7). |
| |
| 作者姓名： | 范大威 李兆鹏 蒋信予 |
| |
| 作者单位： | 中国科学技术大学计算机科学与技术学院,合肥,230026;中国科学技术大学苏州研究院软件安全实验室,江苏苏州,215123 |
| |
| 基金项目： | 国家自然科学基金项目(90718026,60928004)资助 |
| |
| 摘 要： | 出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.
|
| 关 键 词： | 规范转换 代码优化 数据流分析 出具证明编译器 |
Code Optimization and Specification Transformation in Certifying Compiler |
| |
| FAN Da-wei,LI Zhao-peng,JIANG Xan-yu.Code Optimization and Specification Transformation in Certifying Compiler[J].Mini-micro Systems,2011,32(7). |
| |
| Authors: | FAN Da-wei LI Zhao-peng JIANG Xan-yu |
| |
| Affiliation: | FAN Da-wei1,2,LI Zhao-peng1,JIANG Xin-yu1,21(School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China)2(Software Security Laboratory,Suzhou Institute for Advanced Study,Suzhou 215132,China) |
| |
| Abstract: | As an important research field of program verification,certifying compiler is an increasing concern by many researchers of software security.However,current researches mostly focus on the design of program logic and automated theorem proving,while code optimization which we believe is significant for certifying compiler to become practical,is less concerned by the community.In this paper,we propose a dataflow analysis based method to transform specification to pass the constraint of original specification t... |
| |
| Keywords: | specification transformation code optimization data flow analysis certifying compiler |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
