ACL2 meets the GPU: formalizing a CUDA-based parallelizable all-pairs shortest path algorithm in ACL2

DOI10.4204/EPTCS.114.10MaRDI QIDQ6587259zbMATH OpenFDO

Authors David Hardin, Samuel S. Hardin

Publication date 13 August 2024

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Parallel algorithms in computer science (68W10) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Solving path problems on the GPU
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• Automated verification of the parallel Bellman-Ford algorithm
• Automated verification of functional correctness of race-free GPU programs
• Utilization of OpenCL for large graph problems on graphics processing unit

Cites work

• Theorem Proving in Higher Order Logics

This page was built for publication: ACL2 meets the GPU: formalizing a CUDA-based parallelizable all-pairs shortest path algorithm in ACL2

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