软件学报

作者：苏婉昀，高冲，古新才，吴志林

单位：苏婉昀，计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004911,高冲，华为技术有限公司 编程语言实验室, 北京 10008502,古新才，百度 自动驾驶技术部, 北京 10019303,吴志林，计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004904

关键词：分离逻辑;形状性质;线性算术数据约束;集合数据约束;可满足性问题;蕴涵问题;约束求解器

基金：广东省科技厅新一代人工智能项目（2018B010107004）；国家自然科学基金面上基金（61872340）；法国INRIA-中国科学院国际合作项目VIP

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

来源：2023年第5期

《软件学报》期刊编辑部

查看软件学报杂志2023年第5期