On-board data processing requires increasing computational power not possible to be provided by space-grade processors. According to the ESA funded GPU4S (GPU for Space) activity, embedded GPUs are among the most promising candidate platforms in terms of obtained performance. While GPUs have easy to learn programming models, such as CUDA and OpenCL, their dependence on pointers and dynamic memory allocation make the verification of their software challenging. While formal methods have slowly found their way in CPU programs, such as in SPARK Ada and Frama-C, such tools do not yet support for GPUs. In this project we propose to extend a GPU programming model e.g. CUDA with support for formal proofs of software properties as these are supported in the aforementioned languages. This will allow to increase the confidence in GPU software, as it will support both more powerful static analysis of GPU code, as well as support for dynamic verification at program runtime, for those parts of the code that are not possible to be proven. Our implementation will be open source, as Frama-C and Ada SPARK are, and will be possible to be extended by the community in the future. The implementation of this project will increase considerably the confidence on critical GPU code, e.g. code which can be used in the future to accelerate a vision based navigation algorithm on a GPU, and moreover will reduce the verification and qualification cost of GPU code. In other words, the benefits of the application of formal methods in GPUs will be the same as the ones that can be enjoyed nowadays for CPU code.
