《计算机学报》文章摘要   全文下载
文章题目	一种用于指针程序安全性证明的指针逻辑
作者	陈意云 华保健 葛琳 王志芳
作者单位	(中国科学技术大学计算机科学与技术系 合肥 230026) (中国科学技术大学苏州研究院软件安全实验室 江苏苏州 215123)
发表年份	2008
发表月份	3期(372—380)
文章摘要	摘要 在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架，为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质. 关键词 软件安全；指针逻辑；Hoare逻辑；指针分析；类型系统