Back to University of Twente portal
| 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 |
Abstract
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:
http://referaat.cs.utwente.nl/conference/20/paper/7428/a-case-study-for-gpgpu-program-verification.pdf