| 二维逻辑PPTLSL的可满足性检查 |
| |
| 引用本文： | 陆旭,段振华,田聪.二维逻辑PPTLSL的可满足性检查[J].软件学报,2016,27(3):670-681. |
| |
| 作者姓名： | 陆旭 段振华 田聪 |
| |
| 作者单位： | 西安电子科技大学 计算理论与技术研究所,陕西 西安 710071;西安电子科技大学 综合业务网理论及关键技术国家重点实验室,陕西 西安 710071,西安电子科技大学 计算理论与技术研究所,陕西 西安 710071;西安电子科技大学 综合业务网理论及关键技术国家重点实验室,陕西 西安 710071,西安电子科技大学 计算理论与技术研究所,陕西 西安 710071;西安电子科技大学 综合业务网理论及关键技术国家重点实验室,陕西 西安 710071 |
| |
| 基金项目： | 国家自然科学基金(61322202, 61133001, 61420106004, 91418201) |
| |
| 摘 要： | 由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTLSL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(Separation Logic)与命题投影时序逻辑PPTL(Propositional Projection Temporal Logic),能够描述和验证操作链表的指针程序的时序性质.本文简要回顾了PPTLSL的相关理论,并详细介绍工具SAT-PPTLSL的工作原理.该工具主要利用PPTLSL与PPTL之间构建起来的“同构”关系进行PPTLSL公式的可满足性检查.此外,本文结合一些实例展示了SAT-PPTLSL的执行过程,并通过实验分析了关键参数对SAT-PPTLSL执行效率的影响.
|
| 关 键 词： | 时序逻辑 分离逻辑 指针 二维逻辑 可满足性 |
| 收稿时间： | 2015/7/30 0:00:00 |
| 修稿时间： | 2015/10/20 0:00:00 |
Checking Satisfiability of Two-Dimensional Logic PPTLSL |
| |
| LU Xu,DUAN Zhen-Hua and TIAN Cong.Checking Satisfiability of Two-Dimensional Logic PPTLSL[J].Journal of Software,2016,27(3):670-681. |
| |
| Authors: | LU Xu DUAN Zhen-Hua and TIAN Cong |
| |
| Affiliation: | Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;State Key Laboratory of Integrated Service Networks(Xidian University), Xi'an 710071, China,Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;State Key Laboratory of Integrated Service Networks(Xidian University), Xi'an 710071, China and Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;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. |
| |
| Keywords: | temporal logic separation logic pointer two-dimensional logic satisfiability |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
