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

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 - 28th International Symposium, SAS 2021, Proceedings
EditorsCezara Drăgoi, Suvam Mukherjee, Kedar Namjoshi
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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12913 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

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

Keywords

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

Fingerprint

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

Cite this