A sound and complete abstraction for reasoning about parallel prefix sums

DOI10.1145/2535838.2535882zbMATH Open1284.68387OpenAlexW2022457591MaRDI QIDQ5408435FDOQ5408435

Authors: Nathan Chong, Alastair Donaldson, Jeroen Ketema 

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.850.3891

Recommendations

• Computer Aided Verification
• A complete equational axiomatization for prefix iteration
• Combining Predicate Abstraction with Fixpoint Approximations
• scientific article; zbMATH DE number 7471704
• The quest for equational axiomatizations of parallel composition: status and open problems
• scientific article; zbMATH DE number 4035776
• Artificial Intelligence and Symbolic Computation
• The Saga of the Axiomatization of Parallel Composition
• The parallel complexity of integer prefix summation

zbMATH Keywords

abstractionGPUsformal verificationparallel prefix sum computation

Mathematics Subject Classification ID

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

Cited In (2)

• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• An autonomous data language

Uses Software

• CUDA
• KLEE
• OpenCL
• GPUVerify
• GKLEE
• Rodinia

This page was built for publication: A sound and complete abstraction for reasoning about parallel prefix sums

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408435)