Title
Automated Verification of the Parallel Bellman–Ford Algorithm
Author
Safari, M.
Oortwijn, W.
Huisman, M.
Contributor
Drăgoi C., (editor)
Mukherjee S., (editor)
Namjoshi K., (editor)
Publication year
2021
Abstract
Many real-world problems such as internet routing are actually graph problems. To develop efficient solutions to such problems, more and more parallel graph algorithms are proposed. This paper discusses the mechanized verification of a commonly used parallel graph algorithm, namely the Bellman–Ford algorithm, which provides an inherently parallel solution to the Single-Source Shortest Path problem. Concretely, we verify an unoptimized GPU version of the Bellman–Ford algorithm, using the VerCors verifier. The main challenge that we had to address was to find suitable global invariants of the graph-based properties for automated verification. This case study is the first deductive verification to prove functional correctness of the parallel Bellman–Ford algorithm. It provides the basis to verify other, optimized implementations of the algorithm. Moreover, it may also provide a good starting point to verify other parallel graph-based algorithms.
Subject
Deductive verification
Graph algorithms
Parallel algorithms
GPU
Bellman–Ford
Case study
To reference this document use:
http://resolver.tudelft.nl/uuid:d8cff060-9a5d-411e-a5bb-d0e00d4e8d07
DOI
https://doi.org/10.1007/978-3-030-88806-0_17
TNO identifier
961023
Publisher
Springer Verlag, Cham
ISBN
9783030816858
Source
Static Analysis, 12913 (12913), 346-358
Series
Lecture Notes in Computer Science
Bibliographical note
International Static Analysis Symposium, SAS 2021
Document type
conference paper