The paper Formal verification of parallel prefix sum and stream compaction algorithms in CUDA by Mohsen Safari and Marieke Huisman, was accepted to be published in the journal for Theoretical Computer Science . Here is the link to the paper.