二维逻辑PPTLSL的可满足性检查

• 作者: 段振华 田聪 陆旭
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 时序逻辑 分离逻辑 指针 二维逻辑 可满足性
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 软件形式化方法与应用专题
• 页码范围: 670-681
• 页数: 12页
• 分类号: TP301
• 字数: 9609字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004988

摘要

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