文献检索-宁波市创意产业特色资源库

限定检索结果

检索条件"主题词=自动定理证明器"

共 2 条记录，以下是1-10 订阅

全选清除本页清除全部题录导出标记到"检索档案"

视图：

排序：

用于指针逻辑的自动定理证明器(英文): 收藏
分享
引用; 《软件学报》2009年第8期20卷 2037-2050页; 作者：王振明陈意云王志芳中国科学技术大学计算机科学技术系安徽合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123; 提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自...; 提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.; 来源：详细信息评论

一个用于指针程序验证的自动定理证明器的设计与实现: 收藏
分享
引用; 《小型微型计算机系统》2010年第5期31卷 801-806页; 作者：王振明陈意云王志芳中国科学技术大学计算机科学技术系安徽合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123; 对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自...; 对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.; 来源：详细信息评论

全选清除本页清除全部题录导出标记到“检索档案”

共1页<< <1> >>

聚类工具回到顶部