Automated verification of functional correctness of race-free GPU programs

DOI10.1007/s10817-017-9428-2zbMath1426.68054OpenAlexW2751714866MaRDI QIDQ1703009

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

SMTGPGPUprogram verificationsymbolic execution

Mathematics Subject Classification ID

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

Related Items (3)

A Hoare Logic for GPU Kernels ⋮ Checking data-race freedom of GPU kernels, compositionally ⋮ Automated verification of functional correctness of race-free GPU programs

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Automated verification of functional correctness of race-free GPU programs
• The Daikon system for dynamic detection of likely invariants
• A Hoare Logic for SIMT Programs
• Simplify: a theorem prover for program checking
• Symbolic execution and program testing
• On the Complexity of Linear Arithmetic with Divisibility
• Avoiding exponential explosion
• A Hoare Logic for GPU Kernels
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Foundations of Software Science and Computational Structures

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