A Hoare Logic for GPU Kernels

DOI10.1145/3001834zbMath1367.68066OpenAlexW2592143801MaRDI QIDQ5278201

Kensuke Kojima, Atsushi Igarashi

Publication date: 13 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3001834

zbMATH Keywords

Hoare logicGPU

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical problems of computer architecture (68M07) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Checking data-race freedom of GPU kernels, compositionally ⋮ Automated verification of functional correctness of race-free GPU programs

Uses Software

• Coq
• CUDA
• OpenCL
• GPUVerify
• GKLEE
• KLEE-FP

Cites Work

• Unnamed Item
• Verification of sequential and concurrent programs
• An axiomatic proof technique for parallel programs
• Automated verification of functional correctness of race-free GPU programs
• On the Correctness of the SIMT Execution Model of GPUs
• A Hoare Logic for SIMT Programs
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

This page was built for publication: A Hoare Logic for GPU Kernels