| 摘要: |
| 由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTLSL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(separation logic)与命题投影时序逻辑PPTL(propositional projection temporal logic),能够描述和验证操作链表的指针程序的时序性质.简要回顾了PPTLSL的相关理论,并详细介绍了工具SAT-PPTLSL的工作原理.该工具主要利用PPTLSL与PPTL之间构建起来的同构关系进行PPTLSL公式的可满足性检查.此外,结合一些实例展示了SAT-PPTLSL的执行过程,并通过实验分析了关键参数对SAT-PPTLSL执行效率的影响. |
| 关键词: 时序逻辑 分离逻辑 指针 二维逻辑 可满足性 |
| DOI：10.13328/j.cnki.jos.004988 |
| 分类号: |
| 基金项目:国家自然科学基金(61322202,61133001,61420106004,91418201) |
|
| Checking Satisfiability of Two-Dimensional Logic PPTLSL |
|
LU Xu1,2, DUAN Zhen-Hua1,2, TIAN Cong1,2
|
|
1.Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;2.State Key Laboratory of Integrated Service Networks(Xidian University), Xi'an 710071, China
|
| 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. |
| Key words: temporal logic separation logic pointer two-dimensional logic satisfiability |
