title: | Breadth-First Search: Verifying GPGPU Programs |

keywords: | GPU programming, GPGPU verification, Graph, OpenCL, Parallel algorithm |

topics: | Other |

committee: |
Mohsen Safari
, Marieke Huisman |

## Description

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:

**Input: **

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

- A source vertex *s* in *V*.

**Output:**

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

This project consists of two parts. In the first part, you will design a parallel BFS algorithm and implement it to run on a GPU. The second part is to verify the correctness of the algorithm.

** **

**Task:**

- Design and implement a parallel BFS algorithms on a GPU using OpenCL.
- Formulate the requirements in a formal specification language.
- Verify data race-freedom of the algorithm using VerCors tool.
- Verify functional Correctness of the algorithm using VerCors tool.