| COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器 |
| |
| 作者姓名： | 苏婉昀 高冲 古新才 吴志林 |
| |
| 作者单位： | 计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 100049;华为技术有限公司 编程语言实验室, 北京 100085;百度 自动驾驶技术部, 北京 100193 |
| |
| 基金项目： | 广东省科技厅新一代人工智能项目（2018B010107004）;国家自然科学基金面上基金（61872340）;法国INRIA-中国科学院国际合作项目VIP |
| |
| 摘 要： | 
分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展,已经广泛用于对基础软件(比如操作系统内核等)的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的验证一般同时涉及形状性质(比如单链表、双链表、树等)和数据性质(比如有序性、数据不变性等).主要介绍能对动态数据结构的形状性质与数据约束进行融合推理的分离逻辑求解器COMPSPEN.首先介绍COMPSPEN的理论基础,包括能够同时描述线性动态数据结构的形状性质和数据约束的分离逻辑子集SLIDdata、SLIDdata的可满足性和蕴涵问题的判定算法.然后,介绍COMPSPEN工具的基本框架.
最后,使用COMPSPEN工具进行了实例研究.收集整理了600个测试用例,在这600个测试用例上将COMPSPEN与已有的主流分离逻辑求解器Asterix、S2S、Songbird、SPEN进行了比较.实验结果表明COMPSPEN是唯一能够求解含有集合数据约束的分离逻辑求解器,而且总体来讲,能对线性数据结构上的同时含有形状性质和线性算术数据约...
|
| 关 键 词： | 分离逻辑 形状性质 线性算术数据约束 集合数据约束 可满足性问题 蕴涵问题 约束求解器 |
| 收稿时间： | 2020-08-16 |
| 修稿时间： | 2021-02-04 |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载免费的PDF全文 |
|
