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 language | English |
---|---|
Title of host publication | FormaliSE 21: Proceedings of the 9th International Conference on Formal Methods in Software Engineering |
Pages | 111-123 |
Number of pages | 13 |
Volume | 1 |
ISBN (Electronic) | 9781665439138 |
DOIs | |
Publication status | Published - 24 Jun 2021 |
Event | 9th International Conference on Formal Methods in Software Engineering, FormaliSE 2021 - Online Conference Duration: 18 May 2021 → 21 May 2021 Conference number: 9 |
Conference
Conference | 9th International Conference on Formal Methods in Software Engineering, FormaliSE 2021 |
---|---|
Abbreviated title | FormaliSE 2021 |
City | Online Conference |
Period | 18/05/21 → 21/05/21 |