主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
陆旭,段振华,田聪.二维逻辑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)
作者单位E-mail
陆旭 西安电子科技大学计算理论与技术研究所, 陕西 西安 710071
综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071 
 
段振华 西安电子科技大学计算理论与技术研究所, 陕西 西安 710071
综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071 
zhhduan@mail.xidian.edu.cn 
田聪 西安电子科技大学计算理论与技术研究所, 陕西 西安 710071
综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071 
ctian@mail.xidian.edu.cn 
摘要点击次数: 2116
全文下载次数: 1111
中文摘要:
      由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.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阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利