COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器

苏婉昀; 高冲; 古新才; 吴志林

首页> 中文期刊> 《软件学报》 >COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器

COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展,已经广泛用于对基础软件(比如操作系统内核等)的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的验证一般同时涉及形状性质(比如单链表、双链表、树等)和数据性质(比如有序性、数据不变性等).主要介绍能对动态数据结构的形状性质与数据约束进行融合推理的分离逻辑求解器COMPSPEN.首先介绍COMPSPEN的理论基础,包括能够同时描述线性动态数据结构的形状性质和数据约束的分离逻辑子集SLIDdata、SLIDdata的可满足性和蕴涵问题的判定算法.然后,介绍COMPSPEN工具的基本框架.最后,使用COMPSPEN工具进行了实例研究.收集整理了600个测试用例,在这600个测试用例上将COMPSPEN与已有的主流分离逻辑求解器Asterix、S2S、Songbird、SPEN进行了比较.实验结果表明COMPSPEN是唯一能够求解含有集合数据约束的分离逻辑求解器,而且总体来讲,能对线性数据结构上的同时含有形状性质和线性算术数据约束的分离逻辑公式的可满足性问题进行高效的求解,另外,也能对蕴涵问题进行求解.

著录项

来源
《软件学报》 |2023年第5期|2181-2195|共15页
作者
苏婉昀; 高冲; 古新才; 吴志林;
展开▼
作者单位

计算机科学国家重点实验室(中国科学院软件研究所);

中国科学院大学;

华为技术有限公司编程语言实验室;

百度自动驾驶技术部;

展开▼
原文格式 PDF
正文语种 chi
中图分类理论、方法;
关键词
分离逻辑; 形状性质; 线性算术数据约束; 集合数据约束; 可满足性问题; 蕴涵问题; 约束求解器;

相似文献

中文文献
外文文献
专利

1. 基于多级分离技术求解命题逻辑推理的粘贴DNA算法 [J] . 李红 ,袁太生 ,田国瑞 . 现代工业经济和信息化 . 2015,第4期
2. 基于SMT求解器的微处理器指令验证数据约束生成技术 [J] . 谭坚 ,罗巧玲 ,王丽一 . 计算机研究与发展 . 2020,第12期
3. 如何有效进行逻辑推理和判断——谈大学英语听力测试逻辑推理类对话题解题技巧 [J] . 李海云 . 英语自学 . 2007,第004期
4. 新课标下逻辑用语在培养逻辑推理素养中的渗透--以“充分条件与必要条件”在概念与性质教学中的渗透为例 [J] . 张宏杰 ,蒋强军 . 中学数学研究(华南师范大学):下半月 . 2022,第10期
5. 回溯推理的逻辑结构与逻辑性质 [J] . 李延铸 . 社会科学研究 . 1991,第006期
6. 带归纳定义的分离逻辑公式求解器COMPSPEN [C] . GAO Chong ,高冲 ,GU Xincai . 第十六届全国软件与应用学术会议 . 2017
7. 基于矛盾体分离的命题逻辑动态自动演绎推理求解系统研究 [A] . 陈青山 . 2018

COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器

摘要

著录项

相似文献

相关主题

期刊订阅