GPUVerify

swMATH11260MaRDI QIDQ23206FDOQ23206

Author name not available (Why is that?)

Official website: http://multicore.doc.ic.ac.uk/tools/GPUVerify/

Described by source

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

Cited In (41)

• 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
• OpenCL
• Chalice
• Cumapz
• InvGen
• VerCors
• CMC
• CUDPP
• GKLEE
• CUDA-lite
• Rodinia
• TCT
• libFAUDES
• c2i
• REFINER
• KLEE-FP
• Pochoir
• AstraVer
• Gunrock
• BARRACUDA
• CURD
• GMRace
• GRace
• Simulee
• RVT
• MuDiv
• PESTS
• Loopy
• WebAssembly
• Oclgrind
• A sound and complete abstraction for reasoning about parallel prefix sums
• Verification of concurrent systems with VerCors
• A Hoare Logic for GPU Kernels

This page was built for software: GPUVerify