Write a Blog >>
FormaliSE 2021
Tue 18 - Fri 21 May 2021
co-located with ICSE 2021
Wed 19 May 2021 16:00 - 16:30 at FormaliSE Room - Program verification

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.

Wed 19 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Information for Participants
Wed 19 May 2021 15:30 - 17:00 at FormaliSE Room - Program verification
Info for room FormaliSE Room:

Go directly to this room on Clowdr