Automated verification of functional correctness of race-free GPU programs
type: Item
instance of: scholarly article
title: Automated verification of functional correctness of race-free GPU programs
zbMATH Open document ID: 1426.68054
author: Kensuke Kojima
author: Akifumi Imanishi
author: Atsushi Igarashi
published in: Journal of Automated Reasoning
publication date: 2018-03-01T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6845816
zbMATH Keywords: program verification
zbMATH Keywords: GPGPU
zbMATH Keywords: SMT
zbMATH Keywords: symbolic execution
describes a project that uses: Daikon
describes a project that uses: SIMPLIFY
describes a project that uses: Houdini
describes a project that uses: CUDA
describes a project that uses: Why3
describes a project that uses: GKLEE
describes a project that uses: CIL
MaRDI profile type: Publication
full work available at URL: s10817-017-9428-2
OpenAlex ID: W2751714866
cites work: Simplify: a theorem prover for program checking
cites work: Foundations of Software Science and Computational Structures
cites work: The Daikon system for dynamic detection of likely invariants
cites work: Q2763999
cites work: Avoiding exponential explosion
cites work: Symbolic execution and program testing
cites work: A Hoare Logic for SIMT Programs
cites work: A Hoare Logic for GPU Kernels
cites work: On the Complexity of Linear Arithmetic with Divisibility
cites work: Quantified Invariant Generation Using an Interpolating Saturation Prover
cites work: Q4738390
DOI: 10.1007/S10817-017-9428-2
description: scientific article; zbMATH DE number 6845816