%0 Journal Article
%T 一种用于指针程序验证的指针逻辑
%A 陈意云？
%A 李兆鹏？
%A 王志芳？
%A 华保健？
%J 软件学报
%P 415-426
%D 2010
%X 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.
%K 软件安全
%K hoare逻辑
%K 指针逻辑
%K 携带证明的代码
%K 出具证明的编译器
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3620&flag=1