GPUVerify

swMATH11260MaRDI QIDQ23206

No author found.

Described by source

• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

Related Items (12)

Formal verification of parallel prefix sum and stream compaction algorithms in CUDA ⋮ A Hoare Logic for GPU Kernels ⋮ Checking data-race freedom of GPU kernels, compositionally ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Automated verification of the parallel Bellman-Ford algorithm ⋮ Natural projection as partial model checking ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms ⋮ A sound and complete abstraction for reasoning about parallel prefix sums ⋮ Verification of Concurrent Systems with VerCors ⋮ Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms ⋮ Verifying Whiley programs with Boogie

This page was built for software: GPUVerify