二维逻辑PPTL^SL的可满足性检查

来源：软件学报杂志2016年第3期北京时间：

作者：陆旭,段振华,田聪

单位：陆旭，西安电子科技大学计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007111,段振华，西安电子科技大学计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007102,田聪，西安电子科技大学计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007103

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

关键词：时序逻辑;分离逻辑;指针;二维逻辑;可满足性

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