一种基于栈区内存模型的C程序别名判断算法

摘要：

C语言中的指针导致C程序中会出现表达式别名的情况.在基于演绎推理的程序验证中,使用Hoare逻辑的赋值规则前必须消除断言中的别名.别名增加了程序验证的难度.本文根据C语言的语义提出了一种栈区内存模型,可以精确地跟踪栈区的多种类型的表达式,包括取地址、多级解引用、指针关系运算、结构体和数组等.基于上述内存模型,本文提出了一种判断别名的算法,使得验证工具在使用Hoare逻辑的赋值公理之前可以准确的消除断言中的别名.目前该模型已经在一个名为Safe-C验证器的程序验证工具中实现,并且成功验证了多例经典程序.

关键词：程序验证、Hoare逻辑、内存模型、别名、栈区

所属期刊栏目：40

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目 61170018, 61229201 资助

在线出版日期：2019-05-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：353-358