二维逻辑PPTL^SL的可满足性检查

来源 :软件学报 | 被引量 : 0次 | 上传用户：elenganse

【摘要】

：

由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTL^SL是一种二维（时间和空间）时序逻辑,它结合了分离逻辑（separation logic）与命

【作者】

：

陆旭段振华田聪

【机构】

：

西安电子科技大学计算理论与技术研究所,综合业务网理论及关键技术国家重点实验室（西安电子科技大学）

【出处】

：

软件学报

【发表日期】

：

2016年3期

【关键词】

：

时序逻辑分离逻辑指针二维逻辑可满足性 temporal logic separation logic pointer two-dimensional l

【基金项目】

：

国家自然科学基金（61322202,61133001,61420106004,91418201）

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTL^SL是一种二维（时间和空间）时序逻辑,它结合了分离逻辑（separation logic）与命题投影时序逻辑PPTL（propositional projection temporal logic）,能够描述和验证操作链表的指针程序的时序性质.简要回顾了PPTL^SL的相关理论,并详细介绍了工具SAT-PPTL^SL的工作原理.该工具主要利用PPTL^SL与PPTL之间构建起来的同构关系进行PPTL^SL公

其他文献

对高职高专院校计算机教学中几个问题的探讨

为了使高职高专院校的计算机教育能与人力资源市场对IT类毕业生的需求相适应．迫切需要进行教学改革，在改革的过程中存在着一些共性的、常见的问题．有必要对其进行分析与探讨。

期刊

高职高专计算机教育

合作学习在计算机教学中的应用

文章从多元化教案设计、引导式课堂教学、全方位评价体系三方面探讨合作学习在计算机教学中的应用,促进计算机课程教学内容、教学手段、教学方法改革,力争形成计算机课程教学

期刊

合作学习计算机教学

银行卡伪造盗刷纠纷中的民事责任--基于100份裁判文书的实证研究

司法实践对银行卡盗刷案件的责任性质认定存在多种解释路径,导致银行与持卡人之间的责任分配陷入了困境。对债权准占有清偿理论进行分析可知,此类案件的责任性质为拒绝履行下

期刊

银行卡伪造盗刷实证研究债权准占有责任分配

武术继承与创新之间的关系

中华武术源远流长，是东方文明在现代体育运动中的典型代表，有着鲜明的民族文化特色，是一种独特的历史文化现象。文章运用文献资料法并结合自己多年的武术学习与实践，对武术继承与

期刊

武术继承创新关系

超微银粉烧结法

介绍了超微银粉烧结过程,并且给出了用BET等温吸附方法测量烧结物表面积的结果.

期刊

银粉烧结低温试验边界热阻low temperature tests sintering thermal boundary resistance t

职业教育中的新视点：媒体与设计艺术

随着中国经济与国际经济融合的程度越来越高，人们的生活水准和生活品位进一步提升，对产品的包装和设计要求更高。媒体与设计艺术这一新兴学科应运而生，教育者必须明确这门学科的

期刊

媒体与设计艺术学科设置学力要求中等职业教育人文精神

论高校青年女教师的培养

加强对高校女教师的培养,已成为高校稳定、可持续发展的一个重要的课题.本文通过分析青年女教师的发展现状及自身优势与不足,希望找到合理培养青年女教师的方法.

期刊

青年女教师培养高校可持续发展自身优势发展现状

RB模型实例集上置信传播算法的收敛性

置信传播算法求解RB（k,n，a,rc,p）模型实例时非常有效，几乎能够有效求解接近可满足性相变点的难解实例．然而，因子图带有回路的实例，置信传播算法不总有效，常表现为不收敛,对于这种现象

期刊

置信传播算法收敛性约束可满足性问题RB模型belief propagation algorithm convergence constraint s

二维逻辑PPTL^SL的可满足性检查

其他学术论文