A sound and complete abstraction for reasoning about parallel prefix sums

DOI10.1145/2535838.2535882MaRDI QIDQ5408435zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(2)

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

Describes a project that uses

Uses Software

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

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)