二维逻辑PPTLSL的可满足性检查
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(61322202,61133001,61420106004,91418201)


Checking Satisfiability of Two-Dimensional Logic PPTLSL
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61322202, 61133001, 61420106004, 91418201)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTLSL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(separation logic)与命题投影时序逻辑PPTL(propositional projection temporal logic),能够描述和验证操作链表的指针程序的时序性质.简要回顾了PPTLSL的相关理论,并详细介绍了工具SAT-PPTLSL的工作原理.该工具主要利用PPTLSL与PPTL之间构建起来的同构关系进行PPTLSL公式的可满足性检查.此外,结合一些实例展示了SAT-PPTLSL的执行过程,并通过实验分析了关键参数对SAT-PPTLSL执行效率的影响.

    Abstract:

    Programs become more error-prone with inappropriate management of memory because of pointer aliasing, e.g., dereferencing null or dangling pointers, and memory leaks.PPTLSL is a two-dimensional(spatial and temporal) logic which integrates separation logic with PPTL(propositional projection temporal logic).It is useful to describe and verify temporal properties of list manipulating programs.This paper first gives an overview of PPTLSL, and then introduces the foundation of the tool SAT-PPTLSL in detail.SAT-PPTLSL can be used to check the satisfiability of PPTLSL formulas according to the "isomorphic" relationship between PPTLSL and PPTL.In addition, the paper presents examples to show the checking process of SAT-PPTLSL and analyze the effect of some key parameters on the performance of SAT-PPTLSL.

    参考文献
    相似文献
    引证文献
引用本文

陆旭,段振华,田聪.二维逻辑PPTLSL的可满足性检查.软件学报,2016,27(3):670-681

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2015-07-30
  • 最后修改日期:2015-10-20
  • 录用日期:
  • 在线发布日期: 2016-01-06
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号