Separating Separation Logic - Modular Verification of Red-Black Trees.

Interactive theorem provers typically use abstract algebraic data structures to focus on algorithmic correctness. Verification of programs in real programming languages also has to deal with pointer structures, aliasing and, in the case of C, memory management. While progress has been made by using Separation Logic, direct verification of code still has to deal with both aspects at once. In this paper, we show a refinement-based approach that separates the two issues by using a suitable modular structure. We exemplify the approach with a correctness proof for red-black trees, demonstrating that our approach can generate efficient C code that uses parent pointers and avoids recursion. The proof is split into a large part almost identical to high-level algebraic proofs and a separate small part that uses Separation Logic to verify primitive operations on pointer structures.