|author:||Steven de Heus|
|title:||A Case Study for GPGPU Program Verification|
|keywords:||GPU, verification, permissions|
|topics:||Algorithms and Data Structures , Case studies and Applications|
Marina Zaharieva-Stojanovski ,
The goal of this research is to design a concurrent program that computes the edit distance between two strings and then verify the correctness of the program. The program is implemented in OpenCL and specification and verifica- tion is done using permission-based separation logic. The logic used for the (manual) verification is the same as used in the VerCors tool set, which is currently under develop- ment. The results of this research will assist in further development of VerCors.
For the paper see: