Sciweavers

JIP
2016
64views more  JIP 2016»
8 years 1 months ago
Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq
: We design a concurrent separation logic for GPGPU, namely GPUCSL, and prove its soundness by using Coq. GPUCSL is based on a CSL proposed by Blom et al., which is for automatic v...
Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani