Formally Verified Low-Level C Implementation of Crit-Bit Trees in a Live Verification Tool

Abstract

Using a recent live verification tool, we implement a crit-bit tree in C syntax and verify the implementation against the Bedrock2 C-like semantics. This is the first formally verified implementation of crit-bit trees, the first implementation of an efficient key-value store in Bedrock2, and one of only a limited number of formally verified low-level, imperative implementations of a map data structure in general. Our work is the first significant case study of the recent live verification tool. In our benchmarks for lookup, insertion, and deletion, our crit-bit tree implementation was at most 22 % slower than std::map in libstdc++.