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

作者简介:

苏婉昀(1997-),女,硕士,主要研究领域为分离逻辑约束求解;高冲(1994-),男,硕士,主要研究领域为编程语言;古新才(1991-),男,硕士,主要研究领域为分布式计算;吴志林(1980-),男,博士,研究员,博士生导师,CCF专业会员,主要研究领域为自动推理,程序验证,自动机理论

通讯作者:

苏婉昀,suwy@ios.ac.cn

中图分类号:

TP301

基金项目:

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


COMPSPEN: Separation Logic Solver for Integrated Reasoning about Shape Properties and Data Constraints
Author:
Affiliation:

Fund Project:

Guangdong Science and Technology Department grant(No. 2018B010107004); the NSFC grant(No. 61872340); the INRIA-CAS joint research project VIP

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    Separation logic is an extension of the classical Hoare logic for reasoning about pointers and dynamic data structures, and has been extensively used in the formal analysis and verification of fundamental software, including operating system kernels. Automated constraint solving is one of the key means to automate the separation-logic based verification of these programs. The verification of programs manipulating dynamic data structures usually involves both the shape properties, e.g., singly or doubly linked lists and trees, and data constraints, e.g., sortedness and the invariance of data sets/multisets. This paper introduces COMPSPEN, a separation logic solver capable of simultaneously reasoning about the shape properties and data constraints of linear dynamic data structures. First, the theoretical foundations of COMPSPEN are introduced, including the definition of separation logic fragment SLIDdata as well as the decision procedures of the satisfiability and entailment problems of SLIDdata. Then, the implementation and the architecture of the COMPSPEN tool are presented. At last, the experimental results for COMPSEN are reported. 600 test cases are collected and the performance of COMPSPEN is compared with the state-of-the-art separation logic solvers, including Asterix, S2S, Songbird, and SPEN. The experimental results show that COMPSPEN is the only tool capable of solving separation logic formulae involving set data constraints, and in overall, it is able to efficiently solve the satisfiability problem of separation logic formulas involving both shape properties and linear arithmetic data constraints on linear dynamic data structures, and is also capable of solving the entailment problem.

    参考文献
    相似文献
    引证文献
引用本文

苏婉昀,高冲,古新才,吴志林. COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器.软件学报,2023,34(5):2181-2195

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2020-08-16
  • 最后修改日期:2021-02-04
  • 录用日期:
  • 在线发布日期: 2021-08-02
  • 出版日期: 2023-05-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号