ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2 - David S. Hardin; Samuel S. Hardin (ACL2, 2013)