Steven de Heus - A Case Study for GPGPU Program Verification

author:Steven de Heus
title:A Case Study for GPGPU Program Verification
keywords:GPU, verification, permissions
topics:Case studies and Applications, Algorithms and Data Structures
committee:prof.dr. M. Huisman (1st supervisor)
M. Zaharieva-Stojanovski MSc
S. Darabi MSc
graduation date:1 January 2014


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: