Automated verification of the parallel Bellman-Ford algorithm

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

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

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?)

Cited In (3)

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

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)