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

作者简介:

通讯作者:

苏婉昀,suwy@ios.ac.cn

基金项目:

广东省科技厅新一代人工智能项目“高可信深度学习:理论与技术”(2018B010107004);国家自然科学基金面上基金项目(61872340);法国INRIA-中国科学院国际合作项目VIP


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

Fund Project:

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

    分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展,已经广泛用于对基础软件(比如操作系统内核等)的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的验证一般同时涉及形状性质(比如单链表、双链表、树等)和数据性质(比如有序性、数据不变性等).本论文主要介绍能对动态数据结构的形状性质与数据约束进行融合推理的分离逻辑求解器COMPSPEN.我们首先介绍COMPSPEN的理论基础,包括能够同时描述线性动态数据结构的形状性质和数据约束的分离逻辑子集SLIDdata、SLIDdata的可满足性和蕴涵问题的判定算法.然后,我们介绍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, We first introduce the theoretical foundations of COMPSPEN, including the definition of separation logic fragment SLIDdata as well as the decision procedures of the satisfiability and entailment problems of SLIDdata. Then, we present the implementation and the architecture of the COMPSPEN tool. At last, we report the experimental results for COMPSEN. We collected 600 test cases and compared the performance of COMPSPEN against the state-of-the-art separation logic solvers, including ASTERIX, S2S, Songbird, and SPEN. The experimental results showed 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.软件学报,,():0

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

京公网安备 11040202500063号