Formal Verification of Concurrent Binary Search Tree

Concurrent data structures are considered quite hard to design. Programs that use them can have multiple interleaving between thread operations which make reasoning about the correctness of such program difficult. In this thesis, we formally verify two concurrent binary search tree algorithms: a blocking algorithm using fine-grained locking, and a lock-free algorithm us-ing C11 atomic operations. We prove the correctness of the algorithms by formally specifying and verifying their C implementations using the Verified Software Toolchain which supports reasoning about concurrent C programs in the style of the Iris Concurrent Separation logic. All the proofs of correctness have been completed with pen-and-paper and partly mechanized in Coq. The result is the first C-level mechanized verification of concurrent binary search trees