Automated Verification of the Parallel Bellman–Ford Algorithm

Mohsen Safari; Wytse Oortwijn; Marieke Huisman

doi:10.1007/978-3-030-88806-0_17

Automated Verification of the Parallel Bellman–Ford Algorithm

Mohsen Safari, Wytse Oortwijn, Marieke Huisman^*

^*Corresponding author for this work

Formal Methods and Tools

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

267 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 language	English
Title of host publication	Static Analysis
Subtitle of host publication	28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings
Editors	Cezara Drăgoi, Suvam Mukherjee, Kedar Namjoshi
Place of Publication	Cham
Publisher	Springer
Pages	346-358
Number of pages	13
ISBN (Electronic)	978-3-030-88806-0
ISBN (Print)	978-3-030-88805-3
DOIs	https://doi.org/10.1007/978-3-030-88806-0_17
Publication status	Published - 13 Oct 2021
Event	28th International Symposium on Static Analysis, SAS 2021 - Chicago, United States Duration: 17 Oct 2021 → 19 Oct 2021 Conference number: 28

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12913
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	28th International Symposium on Static Analysis, SAS 2021
Abbreviated title	SAS 2021
Country/Territory	United States
City	Chicago
Period	17/10/21 → 19/10/21

Keywords

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

Access to Document

10.1007/978-3-030-88806-0_17

ArticleFinal published version, 895 KBLicence: Taverne

Cite this

Safari, M., Oortwijn, W., & Huisman, M. (2021). Automated Verification of the Parallel Bellman–Ford Algorithm. In C. Drăgoi, S. Mukherjee, & K. Namjoshi (Eds.), Static Analysis: 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings (pp. 346-358). (Lecture Notes in Computer Science; Vol. 12913). Springer. https://doi.org/10.1007/978-3-030-88806-0_17

@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, 2024 OA procedure",

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, 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",

address = "Germany",

}

Safari, M, Oortwijn, W & Huisman, M 2021, Automated Verification of the Parallel Bellman–Ford Algorithm. in C Drăgoi, S Mukherjee & K Namjoshi (eds), Static Analysis: 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12913, Springer, Cham, pp. 346-358, 28th International Symposium on Static Analysis, SAS 2021, Chicago, Illinois, United States, 17/10/21. https://doi.org/10.1007/978-3-030-88806-0_17

Automated Verification of the Parallel Bellman–Ford Algorithm. / Safari, Mohsen; Oortwijn, Wytse; Huisman, Marieke.
Static Analysis: 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings. ed. / Cezara Drăgoi; Suvam Mukherjee; Kedar Namjoshi. Cham: Springer, 2021. p. 346-358 (Lecture Notes in Computer Science; Vol. 12913).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Automated Verification of the Parallel Bellman–Ford Algorithm

AU - Safari, Mohsen

AU - Oortwijn, Wytse

AU - Huisman, Marieke

N1 - Conference code: 28

PY - 2021/10/13

Y1 - 2021/10/13

N2 - 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.

AB - 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.

KW - Bellman–Ford

KW - Case study

KW - Deductive verification

KW - GPU

KW - Graph algorithms

KW - Parallel algorithms

KW - 2024 OA procedure

UR - http://www.scopus.com/inward/record.url?scp=85118140015&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-88806-0_17

DO - 10.1007/978-3-030-88806-0_17

M3 - Conference contribution

AN - SCOPUS:85118140015

SN - 978-3-030-88805-3

T3 - Lecture Notes in Computer Science

SP - 346

EP - 358

BT - Static Analysis

A2 - Drăgoi, Cezara

A2 - Mukherjee, Suvam

A2 - Namjoshi, Kedar

PB - Springer

CY - Cham

T2 - 28th International Symposium on Static Analysis, SAS 2021

Y2 - 17 October 2021 through 19 October 2021

ER -

Automated Verification of the Parallel Bellman–Ford Algorithm

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this