Ctrl K

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

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

1
contributor

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.

Logo of Permission-based Verification of Red-Black Trees and Their Merging - Code
Keywords
Deductive verification
magic wand
producer-consumer pattern
red-black tree
Separation Logic
VerCors
License
  • CC0-1.0
</>Source code
Not specified
Packages

Contributors

LA

Member of community

4TU