LLRB算法的函数式建模及其机械化验证
CSTR:
作者:
作者单位:

作者简介:

左正康(1980-), 男, 博士, 副教授, CCF高级会员, 主要研究领域为形式化方法, 智能化软件. ;黄志鹏(1998-), 男, 硕士, 主要研究领域为定理证明, 形式化方法. ;黄箐(1984-), 男, 博士, 副教授, CCF专业会员, 主要研究领域为智能化软件. ;孙欢(1997-), 女, 硕士生, CCF学生会员, 主要研究领域为定理证明, 形式化方法. ;曾志城(1999-), 男, 硕士生, 主要研究领域为定理证明, 形式化方法. ;胡颖(1998-), 女, 硕士, 主要研究领域为定理证明, 形式化方法. ;王昌晶(1977-), 男, 博士, 教授, 博士生导师, CCF高级会员, 主要研究领域为高可信软件, 智能化软件.

通讯作者:

王昌晶, E-mail: wcj@jxnu.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(61862033, 62262031); 江西省自然科学基金(20212BAB202018); 江西省教育厅科技重点项目(GJJ210307)


Functional Modeling and Mechanized Verification of LLRB Algorithm
Author:
Affiliation:

Fund Project:

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

    基于机器定理证明的形式化验证技术不受状态空间限制, 是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法. LLRB (left-leaning red-black trees)是一种二叉搜索树变体, 其结构比传统的红黑树添加了额外的左倾约束条件, 在验证时无法使用常规的证明策略, 需要更多的人工干预和努力, 其正确性验证是一个公认的难题. 为此, 基于二叉搜索树类算法Isabelle验证框架, 对其附加性质部分进行细化, 并给出具体化的验证方案. 在Isabelle中对LLRB插入和删除操作进行函数式建模, 对其不变量进行模块化处理, 并验证函数的正确性. 这是首次在Isabelle中对函数式LLRB插入和删除算法进行机械化验证, 相较于目前LLRB算法的Dafny验证, 定理数由158减少至84, 且无需构造中间断言, 减轻了验证的负担; 同时, 为复杂树结构算法的函数式建模及验证提供了一定的参考价值.

    Abstract:

    Unlimited by the state and space, the formal verification technology based on mechanized theorem proof is an important method to ensure software correctness and avoid serious loss from potential software bugs. LLRB (left-leaning red-black trees) is a variant of binary search trees, and its structure has an additional left-leaning constraint over the traditional red-black trees. During verification, conventional proof strategies cannot be employed, which requires more manual intervention and effort. Thus, the LLRB correctness verification is widely acknowledged as a challenging problem. To this end, based on the Isabelle verification framework for the binary search tree algorithm, this study refines the additional property part of the framework and provides a concrete verification scheme. The LLRB insertion and deletion operations are functionally modeled in Isabelle, with modular treatment of the LLRB invariants. Subsequently, the function correctness is verified. This is the first mechanized verification of functional LLRB insertion and deletion algorithms in Isabelle. Compared to the current Dafny verification of the LLRB algorithm, the theorem number is reduced from 158 to 84, and it is unnecessary for constructing intermediate assertions, which alleviates the verification burden. Meanwhile, this study provides references for functional modeling and verification of complex tree structure algorithms.

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

左正康,黄志鹏,黄箐,孙欢,曾志城,胡颖,王昌晶. LLRB算法的函数式建模及其机械化验证.软件学报,2024,35(11):5016-5039

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

京公网安备 11040202500063号