一种用于类C语言环境的安全的类型化内存模型

作者：何炎祥; 吴伟; 陈勇; 李清安; 刘健博

来源：Z201211028, 2012, 49(11): 2440-2449.

• 操作语义
• 形式化验证
• 内存模型
• 霍尔逻辑
• 内存安全 operational semantics
• formal verification
• memory model
• Hoare logic
• memory safety

使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理...

• 单位
  武汉大学; 软件工程国家重点实验室