Proving data-parallel programs correct: the proof outlines approach

We present a proof outline generation system for a simple data-parallel kernel language called L. Proof outlines for L are very similar to those for usual scalar-like languages. In particular, they can be mechanically generated backwards from the final post-assertion of the program. They appear thus as a valuable basis to implement a validation assistance tool for data-parallel programming. The equivalence between proof outlines and the sound and complete Hoare logic defined for L in previous papers is also discussed