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

DOI:10.4121/13611578.v1
The DOI displayed 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)