Harish’ Algorithm is the first GPGPU implementation of the Breadth-First Search al- gorithm for graphs. This thesis focuses on verifying data race freedom and functional correctness of Harish’ algorithm using VerCors, a tool to verify parallel and distributed software developed at University of Twente. It was found beforehand that there are two data race conditions present in Harish’s algorithm, which were resolved first. Method contracts using pre- and postconditions and permissions for variables were used to im- plement the fixed algorithm in PVL, the language used for VerCors, to verify data race freedom successfully. For this a different data structure than used originally in Harish’s algorithm was developed that focussed on graph edges instead of vertices. This was done to help VerCors with verifying and also balances the total workload across all threads for increased efficiency. Then this implementation was used as input for an attempt to verify functional correctness using first a recursive path finding algorithm, and secondly operations and ghost variables. Both attempts failed and due to time constraints no further progress was made. Finishing this by introducing lemmas or a different data structure is recommended as future work.