Permission-based verification of red-black trees and their merging

Abstract

This paper presents a verification case study, focussing on red-black trees. In particular, we verify a parallel algorithm for merging red-black trees, which uses lists as intermediate representations and which an industrial partner uses to efficiently manage tables of IP addresses. To verify the algorithm, we use the tool VerCors, which uses permission-based separation logic as its logical foundation. Thus, we first needed a suitable specification of the data structure, using that logic. This specification relies on the magic wand operator (a.k.a. separating implication), which is a connective often neglected when discussing separation logic. This paper describes that specification, as well as the verification of the parallel algorithm. It is an interesting case connecting the more academic endeavour of verifying a data structure with the practical one of verifying industrial code.