汇编代码验证中的形式规范自动生成

• 作者: 刘诚 华保健 李兆鹏 葛琳 陈意云
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 出具证明编译器 汇编代码验证 形式规范 Hoare逻辑 前(后)条件
• 年，卷（期）: 2008,（7）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 1219-1224
• 页数: 6页
• 分类号: TP301.2
• 字数: 7294字
• 语种: 中文

摘要

与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明的编译器自动生成汇编级形式规范,从而减轻程序员的负担.使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力.文章主要描述该方法在出具证明编译器中的实现.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学技术系	83	854	16.0	26.0
2	华保健	中国科学技术大学计算机科学技术系	17	116	6.0	10.0
3	刘诚	中国科学技术大学计算机科学技术系	31	296	8.0	17.0
4	李兆鹏	中国科学技术大学计算机科学技术系	17	99	7.0	9.0
5	葛琳	中国科学技术大学计算机科学技术系	10	83	6.0	9.0