Now showing items 1-1 of 1

    • CUDA au Coq: A Framework for Machine-Validating GPU Assembly Programs 

      Ferrell, Benjamin; Duan, Jun; Hamlen, Kevin W. (Institute of Electrical and Electronics Engineers Inc., 2019-03-25)
      A prototype framework for formal, machine-checked validation of GPU pseudo-assembly code algorithms using the Coq proof assistant is presented and discussed. The framework is the first to afford GPU programmers a reliable ...