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

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference [25]
  • |
  • Related [14]
  • | | |
  • Comments
    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.

    Reference
    [1] Leavens GT, Leino KRM, Müller P. Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, 2007, 19(2): 159–189.
    [2] Leino K, Moskal M. VACID-0: Verification of ample correctness of invariants of data-structures, edition 0. In: Proc. of the 2010 Tools and Experiments Workshop at VSTTE. 2010. 221–331.
    [3] 宋丽华, 王海涛, 季晓君, 张兴元. 文件比较算法fcomp在Isabelle/HOL中的验证. 软件学报, 2017, 28(2): 203–215. http://www.jos.org.cn/1000-9825/5098.htm
    Song LH, Wang HT, Ji XJ, Zhang XY. Verification of file comparison algorithm fcomp in Isabelle/HOL. Ruan Jian Xue Bao/Journal of Software, 2017, 28(2): 203–215 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5098.htm
    [4] 江南, 李清安, 汪吕蒙, 张晓瞳, 何炎祥. 机械化定理证明研究综述. 软件学报, 2020, 31(1): 82–112. http://www.jos.org.cn/1000-9825/5870.htm
    Jiang N, Li QA, Wang LM, Zhang XT, He YX. Overview on mechanized theorem proving. Ruan Jian Xue Bao/Journal of Software, 2020, 31(1): 82–112 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5870.htm
    [5] Sedgewick R. Left-leaning red-black trees. In: Proc. of the 2008 Dagstuhl Workshop on Data Structures, 2008. 17–25.
    [6] Peña R. An assertional proof of red-black trees using Dafny. Journal of Automated Reasoning, 2020, 64(4): 767–791.
    [7] Appel A W. Efficient verified red-black trees. 2011. https://www.cs.princeton.edu/~appel/papers/redblack.pdf
    [8] Nipkow T. Automatic functional correctness proofs for functional search trees. In: Proc. of the 7th Int’l Conf. on Interactive Theorem Proving. Springer, 2016. 307–322.
    [9] Reade CMP. Balanced trees with removals: An exercise in rewriting and proof. Science of Computer Programming, 1992, 18(2): 181–204.
    [10] Cormen TH, Leiserson CE, Rivest RL, Stein C. Introduction to Algorithms. 4th ed., Cambridge: MIT Press, 2022.
    [11] Andersson A. Balanced search trees made simple. In: Proc. of the 3rd Workshop on Algorithms and Data Structures. Montreal: Springer, 1993. 60–71.
    [12] Zhao YW. Functional programming and proof. Electronic textbook. 2021. https://www.yuque.com/zhaoyongwang/fpp/
    [13] Okasaki C. Red-black trees in a functional setting. Journal of Functional Programming, 1999, 9(4): 471–477.
    [14] Filliâtre JC, Letouzey P. Functors for proofs and programs. In: Proc. of the 2004 European Symp. on Programming. Barcelona: Springer, 2004. 370–384.
    [15] Bobot F, Filliâtre C, Marché C, Paskevich A. Why3: Shepherd your herd of provers. In: Proc. of the 1st Int’l Workshop on Intermediate Verification Languages. Wroclaw, 2011. 53–64.
    [16] Nipkow T, Blanchette J, Eberl M, Gómez-Londoño A, Lammich P, Sternagel C, Wimmer S, Zhan BH. Functional algorithms, verified! 2021. https://functional-algorithms-verified.org
    [17] Ahmadi R, Leino KRM, Nummenmaa J. Automatic verification of Dafny programs with traits. In: Proc. of the 17th Workshop on Formal Techniques for Java-like Programs. Prague: ACM, 2015. 4.
    [18] Nipkow T, Klein G. Concrete Semantics: With Isabelle/HOL. Springer Int’l Publishing, 2021.
    [19] Back R. Invariant based programming: Basic approach and teaching experiences. Formal Aspects of Computing, 2009, 21(3): 227–244.
    [20] Ballarin C. Tutorial to locales and locale interpretation. Contribuciones Científicas en honor de Mirian Andrés Gómez. Universidad de La Rioja, 2010. 123–140.
    [21] Hoare CAR. Proof of correctness of data representations. In: Gries D, ed. Programming Methodology. New York: Springer, 1978.
    [22] Jones CB. Program specification and verification in VDM. In: Logic of Programming and Calculi of Discrete Design. Berlin: Springer, 1987. 149–184.
    [23] Nipkow T. Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? In: Proc. of the 1987 Annual Symp. on Theoretical Aspects of Computer Science. Passau: Springer, 1987. 260–271.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:734
  • PDF: 2019
  • HTML: 531
  • Cited by: 0
History
  • Received:December 15,2022
  • Revised:March 23,2023
  • Online: December 06,2023
  • Published: November 06,2024
You are the first2043807Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063