The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
doi: 10.4121/13611578

Armborst, Lukas (2021): Permission-based Verification of Red-Black Trees and Their Merging - Code. Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/13611578.v1

Software

• Computer Software

Deductive Verification, magic wand, producer-consumer pattern, red-black tree, Separation Logic, VerCors

CC0

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Lukas Armborst

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.

• 2021-01-21 first online, published, posted

4TU.ResearchData

java source files, annotated with JML-style comments for the VerCors verifier

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science, Formal Methods and Tools (FMT)