@inproceedings{a41cee10068945de9dd7c67001890225,
title = "Automated Verification of the Parallel Bellman–Ford Algorithm",
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.",
keywords = "Bellman–Ford, Case study, Deductive verification, GPU, Graph algorithms, Parallel algorithms",
author = "Mohsen Safari and Wytse Oortwijn and Marieke Huisman",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 28th International Symposium on Static Analysis, SAS 2021 ; Conference date: 17-10-2021 Through 19-10-2021",
year = "2021",
month = oct,
day = "13",
doi = "10.1007/978-3-030-88806-0_17",
language = "English",
isbn = "978-3-030-88805-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "346--358",
editor = "Cezara Dr{\u a}goi and Suvam Mukherjee and Kedar Namjoshi",
booktitle = "Static Analysis",
}