concurrent data structure into concurrency-control and data-structure components, which
can then be modularly combined with no additional proof effort. In this paper, we implement
the template approach in the Verified Software Toolchain (VST), and use it to prove
correctness of C implementations of fine-grained concurrent data structures. This involves
translating code, specifications, and proofs to the idiom of C and VST, and gives us another …