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

Automatic Generation of Formal Specifications in Assembly Code Certification

作　　者：葛琳[1] 陈意云[1] 华保健[1] 李兆鹏[1] 刘诚[1] 

机构地区：[1]中国科学技术大学计算机科学技术系,安徽合肥230027

出　　处：《小型微型计算机系统》2008年第7期1219-1224,共6页Journal of Chinese Computer Systems

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

摘　　要：与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明的编译器自动生成汇编级形式规范,从而减轻程序员的负担.使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力.文章主要描述该方法在出具证明编译器中的实现.The formal specifications in assembly code certification are usually complicated. Some specifications can be automatically generated, but usually lack for expressiveness. Others are too complex to be generated automatically. Such specifications are usually written by programmers and they are a big burden on programmers. This paper presents a method for generating formal specifications automatically. It uses a certifying compiler to generate formal specifications for assembly code, so that programmers are freed from writing specifications for assembly code. The generated specifications are more expressive than those generated automatically by other existent methods. This paper mainly describes the implementation of this method in a certifying compiler.

关 键 词：出具证明编译器 汇编代码验证 形式规范Hoare逻辑 前(后)条件 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]