A Hoare Logic for SIMT Programs

DOI10.1007/978-3-319-03542-0_5zbMath1426.68053OpenAlexW58661141MaRDI QIDQ2937782

Atsushi Igarashi, Kensuke Kojima

Publication date: 12 January 2015

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-03542-0_5

Mathematics Subject Classification ID

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

Related Items (3)

A Hoare Logic for GPU Kernels ⋮ Checking data-race freedom of GPU kernels, compositionally ⋮ Automated verification of functional correctness of race-free GPU programs

Uses Software

• CUDA
• OpenCL
• GKLEE

Cites Work

• Verification of sequential and concurrent programs
• On the Correctness of the SIMT Execution Model of GPUs
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

This page was built for publication: A Hoare Logic for SIMT Programs