GPUVerify

swMATH11260MaRDI QIDQ23206FDOQ23206

Author name not available (Why is that?)

Described by source

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

Cited In (12)

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

This page was built for software: GPUVerify