Formal verification of parallel prefix sum and stream compaction algorithms in CUDA

DOI10.1016/j.tcs.2022.02.027zbMath1483.68091OpenAlexW4214815337MaRDI QIDQ2120963

Marieke Huisman, Mohsen Safari

Publication date: 1 April 2022

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2022.02.027

zbMATH Keywords

CUDAseparation logicdeductive verificationprefix sumGPU verificationstream compaction

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• CUDA
• z3
• VeriFast
• Smallfoot
• VerCors
• GPUVerify
• GKLEE
• Viper
• GRace
• Oclgrind

Cites Work

• Formal verification of parallel stream compaction and summed-area table algorithms
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• A Regular Layout for Parallel Adders
• Permission accounting in separation logic
• A sound and complete abstraction for reasoning about parallel prefix sums
• A Parallel Algorithm for the Efficient Solution of a General Class of Recurrence Equations
• Unnamed Item

This page was built for publication: Formal verification of parallel prefix sum and stream compaction algorithms in CUDA