一种用于指针程序安全性证明的指针逻辑

在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.

A Pointer Logic for Safety Verification of Pointer Programs

Safety is an important issue among the properties of high-assurance software and developing the verification methods for software to meet safety policies is one of the hot research.In terms of the authors' sketch of design and verification of safety programs,a pointer logic system is designed for a subset of C-like language.This logic system is an extension of Hoare logic system and inference rules are designed to express the modification of pointer information for every kind of statements.It can be used for accurate pointer analysis of pointer programs.The information from the analysis can be used to verify if pointer programs satisfy the side conditions of typing rules and then support safety verification for programs.The logic system can also be used to verify other properties of pointer programs.