author: Erwin Everts
title: Verification of the shortest pathfinder algoritm
topics: Case studies and Applications
committee: Marieke Huisman ,
Saeed Darabi
started: September 2015
end: March 2017


PathFinder uses dynamic programming to find a path on a 2-D grid from the bottom row to the top row with the smallest accumulated weights, where each step of the path moves straight ahead or diagonally ahead. It iterates row by row, each node picks a neighboring node in the previous row that has the smallest accumulated weight, and adds its own weight to the sum[Rod].

Goal of this project

Given the impelmentation of Pathfinder for GPUs [OpenCL] from Rodinia Benchmark [Rod]. We want to specifiy and verify data-race freedom and also functional properties of the kernel. We use the technique we previosly developed for reasoning about the correctness of GPU programs [SCP,ByteC0ode]. We use VerCors tool set to automatically verify the specified kernel [VerCors].  



[ByteCode] M. Huisman and M. Mihelcic. Speciļ¬cation and Veriļ¬cation of GPGPUPrograms using Permission-Based Separation Logic. 2013.[.pdf]

[OpenCL] Khronos OpenCLWorking Group. The OpenCL Specification, version 1.2, 2001, URL

[VerCors]A. AmighiS. Blom, M. Huisman, M. Zaharieva-Stojanovski. The VerCors Project. Setting Up Basecamp. In proceedings of Programming Languages meets Program Verification (PLPV 2012). ACM Digital Library. To appear. [.pdf]

[SCP] Stefan, Bloom, M. Huisman and M. Mihelcic, Specification and Verification of GPGPU programs.