Automated verification of the parallel Bellman-Ford algorithm

DOI10.1007/978-3-030-88806-0_17MaRDI QIDQ2145339zbMATH OpenOpenAlexFDO

Authors Mohsen Safari, Wytse Oortwijn, Marieke Huisman

Publication date 17 June 2022

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

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)

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

Cites work

• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• A new approach to incremental cycle detection and related problems
• A note on two problems in connexion with graphs
• Automated verification of parallel nested DFS
• Locality-based relaxation: an efficient method for GPU-based computation of shortest paths
• Multi-core nested depth-first search
• On a routing problem
• Structural analysis of narratives with the Coq proof assistant
• Verified memoization and dynamic programming
• Verifying concurrent graph algorithms

Cited in

(3)

• Verification of correctness of parallel algorithms in practice
• Automated verification of parallel nested DFS
• ACL2 meets the GPU: formalizing a CUDA-based parallelizable all-pairs shortest path algorithm in ACL2

Describes a project that uses

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)