Automated verification of the parallel Bellman-Ford algorithm

DOI10.1007/978-3-030-88806-0_17zbMATH Open1497.68396OpenAlexW3205264255MaRDI QIDQ2145339FDOQ2145339

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

Recommendations

• Automated verification of parallel nested DFS
• scientific article; zbMATH DE number 1057774
• scientific article; zbMATH DE number 1830934
• Verifying concurrent graph algorithms
• Automated verification of functional correctness of race-free GPU programs

zbMATH Keywords

graph algorithmsparallel algorithmsGPUcase studyBellman-Forddeductive verification

Mathematics Subject Classification ID

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

Cites Work

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

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2145339)