title: Breadth-First Search: Verifying GPGPU Programs
keywords: GPGPU verification, Parallel graph algorithm
topics: Case studies and Applications
committee: Mohsen Safari ,
Marieke Huisman


Breadth-First Search (BFS) is a well-known problem in graph theory which has many applications. In this problem, we would like to find the minimum number of edges needed to reach a vertex ‘v’ from a source vertex ‘s’ in a graph ‘G’. The formal definition of the problem is:


-       A graph G=(V, E) where V is the set of vertices and E the set of edges.

-       A source vertex s in V.


-       An array in size of V to indicate the minimum number of edges for each vertex.


Harish's algorithm [1] is the first GPGPU-based implementation of BFS. The goal of this project is to verify the correctness of this implementation. To do that, you need to verify data race freedom and functional correctness using deductive verification approach. 


  1. Understand the GPU-based implementation of BFS.
  2. Formulate the requirements in a formal specification language.
  3. Verify data race-freedom of the algorithm using VerCors tool.
  4. Verify functional Correctness of the algorithm using VerCors tool.


[1] Harish, Pawan, and P. J. Narayanan. "Accelerating large graph algorithms on the GPU using CUDA." International conference on high-performance computing. Springer, Berlin, Heidelberg, 2007.