| 陆旭,段振华,田聪.二维逻辑PPTLSL的可满足性检查.软件学报,2016,27(3):670-681 |
| 二维逻辑PPTLSL的可满足性检查 |
| Checking Satisfiability of Two-Dimensional Logic PPTLSL |
| 投稿时间：2015-07-30 修订日期：2015-10-20 |
| DOI：10.13328/j.cnki.jos.004988 |
| 中文关键词: 时序逻辑 分离逻辑 指针 二维逻辑 可满足性 |
| 英文关键词:temporal logic separation logic pointer two-dimensional logic satisfiability |
| 基金项目:国家自然科学基金(61322202,61133001,61420106004,91418201) |
|
| 摘要点击次数: 3709 |
| 全文下载次数: 1864 |
| 中文摘要: |
| 由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTLSL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(separation logic)与命题投影时序逻辑PPTL(propositional projection temporal logic),能够描述和验证操作链表的指针程序的时序性质.简要回顾了PPTLSL的相关理论,并详细介绍了工具SAT-PPTLSL的工作原理.该工具主要利用PPTLSL与PPTL之间构建起来的同构关系进行PPTLSL公式的可满足性检查.此外,结合一些实例展示了SAT-PPTLSL的执行过程,并通过实验分析了关键参数对SAT-PPTLSL执行效率的影响. |
| 英文摘要: |
| 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. |
|
HTML 下载PDF全文 查看/发表评论 下载PDF阅读器 |
