微信服务号

微信订阅号

2025年3月24日 10:58 星期一
首页 > 过刊浏览>2010年第21卷第2期 >334-343
PDF HTML阅读 XML下载 导出引用 引用提醒
处理指针相等关系不确定的指针逻辑
作者:
基金项目:

Supported by the National Natural Science Foundation of China under Grant Nos.90718026, 60928004 (国家自然科学基金)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [17]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展,可用来对指针程序进行精确的指针分析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质 证明.

    Abstract:

    A pointer logic is designed for a C-like programming language PointerC. The pointer logic is an extension of Hoare logic, and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated. This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets, so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain.

    参考文献
    [1] Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science. Copenhagen: IEEE Computer Society Press, 2002. 55-74.
    [2] Hua BJ, Chen YY, Ge L, Wang ZF. The PointerC programming language specification. Technical Report. http://kyhcs.ustcsz.edu. cn/old/lss/doc/
    [3] Chen YY, Hua BJ, Ge L, Wang ZF. A pointer logic for safety verification of pointer programs. Chinese Journal of Computers, 2008,31(3):372-380 (in Chinese with English abstract).
    [4] Chen YY, Ge L, Hua BJ, Li ZP, Liu C, Wang ZF. A pointer logic and certifying compiler. Frontiers of Computer Science in China, 2007,1(3):297-312.
    [5] Chen YY, Li ZP, Wang ZF, Hua BJ. A pointer logic for verification of pointer programs. Technical Report, 2010. http://kyhcs.ustcsz.edu.cn/lss
    [6] Wang ZF, Chen YY, Wang ZM, Wang W, Tian B. An extension to pointer logic for verification. In: Proc. of the 2nd IEEE/IFIP Int’l Symp. on Theoretical Aspects of Software Engineering. Nanjing: IEEE Computer Society Press, 2008. 49-56.
    [7] Hua BJ, Chen YY, Li ZP, Wang ZF, Ge L. Design and proof of a safe programming language PointerC. Chinese Journal of Computers, 2008,31(4):556-564 (in Chinese with English abstract).
    [8] Chen YY, Ge L, Hua BJ, Li ZP, Liu C. Design of a certifying compiler supporting proof of program safety. In: Proc. of the 1st IEEE/IFIP Int’l Symp. on Theoretical Aspects of Software Engineering. Shanghai: IEEE Computer Society Press, 2007. 127-136.
    [9] Schorr H, Waite WM. An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM, 1967,10(8):501-506.
    [10] Hubert T, Marché C. A case study of C source code verification: The Schorr-Waite algorithm. In: Aichernig BK, Beckert B, eds. Proc. of the 3rd IEEE Int’l Conf. on Software Engineering and Formal Methods. Koblenz: IEEE Computer Society Press, 2005. 190-199.
    [11] The Glibc contributors. http://www.gnu.org/software/libc/
    [12] Liang HJ, Zhang Y, Chen YY, Li ZP, Hua BJ. An example of reasoning in extended pointer logic: AIO remove request function in Glibc. Technical Report. http://home.ustc.edu.cn/～lhj1018/
    [13] Bornat R. Proving pointer programs in Hoare logic. In: Backhouse RC, Oliveira JN, eds. Proc. of the 5th Int’l Conf. on Mathematics of Program Construction. LNCS 1837, Ponte de Lima: Springer-Verlag, 2000. 102-126.
    [14] Bornat R, Calcagno C, O’Hearn PW. Local reasoning, separation and aliasing. In: Proc. of the 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management. 2004.
    [15] Yang H. An example of local reasoning in BI pointer logic: The Schorr-Waite graph marking algorithm. In: Henglein F, Hughes J, Makholm H, Niss H, eds. Proc. of the 1st Workshop on Semantics, Program Analysis and Computing Environments for Memory Management. London: IT University of Copenhagen, 2001. 41-68.
    附中文参考文献: [3] 陈意云,华保健,葛琳,王志芳.一种用于指针程序安全性证明的指针逻辑.计算机学报,2008,31(3):372-380.
    [7] 华保健,陈意云,李兆鹏,王志芳,葛琳.安全语言PointerC的设计及形式证明.计算机学报,2008,31(4):556-564.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

梁红瑾,张昱,陈意云,李兆鹏,华保健.处理指针相等关系不确定的指针逻辑.软件学报,2010,21(2):334-343

复制
分享
文章指标
  • 点击次数:10696
  • 下载次数: 8620
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2009-06-14
  • 最后修改日期:2009-12-07
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19727573位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号