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
committee: Marieke Huisman ,
Marina Zaharieva-Stojanovski ,
Saeed Darabi
end: 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:


Additional Resources

  1. The paper