## Abstract

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.

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 language | English |
---|---|

Title of host publication | NASA Formal Methods |

Subtitle of host publication | 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings |

Editors | Ritchie Lee, Susmit Jha, Anastasia Mavridou |

Place of Publication | Cham |

Publisher | Springer |

Pages | 170-186 |

Number of pages | 17 |

ISBN (Electronic) | 978-3-030-55754-6 |

ISBN (Print) | 978-3-030-55753-9 |

DOIs | |

Publication status | Published - 10 Aug 2020 |

Event | 12th NASA Formal Methods Symposium, NFM 2020 - Virtual Conference Duration: 11 May 2020 → 15 May 2020 Conference number: 12 https://ti.arc.nasa.gov/events/nfm-2020/ |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 12229 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 12th NASA Formal Methods Symposium, NFM 2020 |
---|---|

Abbreviated title | NFM 2020 |

Period | 11/05/20 → 15/05/20 |

Internet address |

## Keywords

- 22/2 OA procedure