Automated Verification of the Parallel Bellman–Ford Algorithm

Mohsen Safari, Wytse Oortwijn, Marieke Huisman*

*Corresponding author for this work

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

3 Citations (Scopus)
214 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationStatic Analysis
Subtitle of host publication28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings
EditorsCezara Drăgoi, Suvam Mukherjee, Kedar Namjoshi
Place of PublicationCham
PublisherSpringer
Pages346-358
Number of pages13
ISBN (Electronic)978-3-030-88806-0
ISBN (Print)978-3-030-88805-3
DOIs
Publication statusPublished - 13 Oct 2021
Event28th International Symposium on Static Analysis, SAS 2021 - Chicago, United States
Duration: 17 Oct 202119 Oct 2021

Publication series

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

Conference

Conference28th International Symposium on Static Analysis, SAS 2021
Country/TerritoryUnited States
CityChicago
Period17/10/2119/10/21

Keywords

  • Bellman–Ford
  • Case study
  • Deductive verification
  • GPU
  • Graph algorithms
  • Parallel algorithms
  • 2024 OA procedure

Fingerprint

Dive into the research topics of 'Automated Verification of the Parallel Bellman–Ford Algorithm'. Together they form a unique fingerprint.

Cite this