Permission-Based Verification of Red-Black Trees and Their Merging

Lukas Armborst*, Marieke Huisman

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

21 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationFormaliSE 21: Proceedings of the 9th International Conference on Formal Methods in Software Engineering
Publication statusAccepted/In press - 2021
Event9th International Conference on Formal Methods in Software Engineering, FormaliSE 2021 - Online Conference
Duration: 18 May 202121 May 2021
Conference number: 9

Conference

Conference9th International Conference on Formal Methods in Software Engineering, FormaliSE 2021
Abbreviated titleFormaliSE 2021
CityOnline Conference
Period18/05/2121/05/21

Fingerprint Dive into the research topics of 'Permission-Based Verification of Red-Black Trees and Their Merging'. Together they form a unique fingerprint.

Cite this