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

DOI10.4204/EPTCS.114.10zbMATH Open1542.68217MaRDI QIDQ6587259FDOQ6587259

Authors: David Hardin, Samuel S. Hardin 

Publication date: 13 August 2024

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

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)

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)