Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
From MaRDI portal
Publication:2120963
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
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
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