TY - DATA
T1 - Permission-based Verification of Red-Black Trees and Their Merging - Code
PY - 2021/01/21
AU - Lukas Armborst
UR - https://data.4tu.nl/articles/software/Permission-based_Verification_of_Red-Black_Trees_and_Their_Merging_-_Code/13611578/1
DO - 10.4121/13611578.v1
KW - Deductive Verification
KW - VerCors
KW - red-black tree
KW - producer-consumer pattern
KW - Separation Logic
KW - magic wand
N2 - These files implement a red-black tree and an algorithm to concurrently merge such trees. The code is written in Java, and annotated with JML-style comments that allow the VerCors verifier to prove the correctness of e.g. inserting and deleting nodes in the tree, and of the merging algorithm.<br>
ER -