https://hgpu.org/?p=9099
Specification and Verification of GPGPU Programs using Permission-Based Separation Logic