%0 Computer Program
%A Armborst, Lukas
%D 2021
%T Permission-based Verification of Red-Black Trees and Their Merging - Code
%U https://data.4tu.nl/articles/software/Permission-based_Verification_of_Red-Black_Trees_and_Their_Merging_-_Code/13611578/1
%R 10.4121/13611578.v1
%K Deductive Verification
%K VerCors
%K red-black tree
%K producer-consumer pattern
%K Separation Logic
%K magic wand
%X 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>
%I 4TU.ResearchData