Formal Verification of Parallel Prefix Sum

Mohsen Safari*, Wytse Oortwijn, Sebastiaan Joosten, Marieke Huisman

*Corresponding author for this work

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

10 Citations (Scopus)
102 Downloads (Pure)


With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.

In this paper, we use deductive program verification based on permission-based separation logic, as supported by VerCors, to show correctness of the two most frequently used parallel in-place prefix sum algorithms for an arbitrary array size. Interestingly, the correctness proof for the second algorithm reuses the auxiliary lemmas that we needed to create the first proof. To the best of our knowledge, this paper is the first tool-supported verification of functional correctness of the two parallel in-place prefix sum algorithms which does not make any assumption about the size of the input array.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings
EditorsRitchie Lee, Susmit Jha, Anastasia Mavridou
Place of PublicationCham
Number of pages17
ISBN (Electronic)978-3-030-55754-6
ISBN (Print)978-3-030-55753-9
Publication statusPublished - 10 Aug 2020
Event12th NASA Formal Methods Symposium, NFM 2020 - Virtual Conference
Duration: 11 May 202015 May 2020
Conference number: 12

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference12th NASA Formal Methods Symposium, NFM 2020
Abbreviated titleNFM 2020
Internet address


  • 22/2 OA procedure


Dive into the research topics of 'Formal Verification of Parallel Prefix Sum'. Together they form a unique fingerprint.

Cite this