Automated verification of the parallel Bellman-Ford algorithm

DOI10.1007/978-3-030-88806-0_17zbMath1497.68396OpenAlexW3205264255MaRDI QIDQ2145339

Mohsen Safari, Marieke Huisman, Wytse Oortwijn

Publication date: 17 June 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-88806-0_17

zbMATH Keywords

parallel algorithmsgraph algorithmscase studyGPUBellman-Forddeductive verification

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Parallel algorithms in computer science (68W10) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Coq
• Dafny
• Isabelle
• Isabelle/HOL
• CUDA
• Why3
• VerCors
• GPUVerify
• GKLEE
• GitHub
• AstraVer
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• A note on two problems in connexion with graphs
• Locality-based relaxation: an efficient method for GPU-based computation of shortest paths
• Verified memoization and dynamic programming
• Structural Analysis of Narratives with the Coq Proof Assistant
• Multi-core Nested Depth-First Search
• Verifying Concurrent Graph Algorithms
• On a routing problem
• A New Approach to Incremental Cycle Detection and Related Problems
• Automated Verification of Parallel Nested DFS

This page was built for publication: Automated verification of the parallel Bellman-Ford algorithm