Automated verification of functional correctness of race-free GPU programs

DOI10.1007/S10817-017-9428-2MaRDI QIDQ1703009zbMATH OpenOpenAlexFDO

Authors Kensuke Kojima, Akifumi Imanishi, Atsushi Igarashi

Publication date 1 March 2018

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-017-9428-2

zbMATH Keywords

GPGPUprogram verificationSMTsymbolic execution

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A Hoare Logic for GPU Kernels
• Checking data-race freedom of GPU kernels, compositionally
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
• A Hoare logic for SIMT programs
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA

Cites work

• A Hoare Logic for GPU Kernels
• A Hoare logic for SIMT programs
• Automated verification of functional correctness of race-free GPU programs
• Avoiding exponential explosion: generating compact verification conditions
• Foundations of Software Science and Computational Structures
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• scientific article; zbMATH DE number 2087570 (Why is no real title available?)
• On the complexity of linear arithmetic with divisibility
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Simplify: a theorem prover for program checking
• Symbolic execution and program testing
• The Daikon system for dynamic detection of likely invariants

Cited in

(10)

• Automated verification of functional correctness of race-free GPU programs
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• Automated verification of the parallel Bellman-Ford algorithm
• A Hoare logic for SIMT programs
• A Hoare Logic for GPU Kernels
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
• Static detection of uncoalesced accesses in GPU programs
• ACL2 meets the GPU: formalizing a CUDA-based parallelizable all-pairs shortest path algorithm in ACL2
• Memory access protocols: certified data-race freedom for GPU kernels
• Checking data-race freedom of GPU kernels, compositionally

Describes a project that uses

Uses Software

• Daikon
• SIMPLIFY
• Houdini
• CUDA
• Why3
• GKLEE
• CIL

This page was built for publication: Automated verification of functional correctness of race-free GPU programs

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