SoftwareApplication
identifier: 10.4121/13611578
name: Permission-based Verification of Red-Black Trees and Their Merging - Code
description: Permission-based Verification of Red-Black Trees and Their Merging - Code
description: 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.
author: https://orcid.org/0000-0001-7565-0954
keywords: Separation Logic
keywords: Deductive verification
keywords: producer-consumer pattern
keywords: VerCors
keywords: magic wand
keywords: red-black tree
license:
  creative work: creativeWork
    name: CC0-1.0

https://orcid.org/0000-0001-7565-0954
type: Person
given name: Lukas
family name: Armborst
name: Lukas Armborst