Permission-based Verification of Red-Black Trees and Their Merging - Code

doi:10.4121/13611578.v1
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
Datacite citation style:
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
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Software
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.
history
  • 2021-01-21 first online, published, posted
publisher
4TU.ResearchData
format
java source files, annotated with JML-style comments for the VerCors verifier
organizations
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science, Formal Methods and Tools (FMT)

DATA

files (9)