欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.
英文摘要：
The increasing demands for high-assurance software make the verification of pointer programs a hot research point. As an extension of Hoare logic,Pointer Logic can be used for accurate pointer analysis of pointer programs. This paper introduces some details in designing and implementing of an automated theorem prover for Pointer Logic,and describes some algorithms. The experimental results show our implementation can fully automatically prove the verification conditions for pointer programs in C-like language and produce machine-checkable proofs. The programs for testing are mainly about singly-linked lists,doubly-linked lists and binary trees.
同期刊论文项目
同项目期刊论文
期刊信息
位置：