Specification and verification of GPGPU programs

No abstract is available for this paper.

• Publication year

  2013

• Venue

  Science of Computer Programming

• Publication date

  2013-11-08

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1016/j.scico.2014.03.013
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Axiomatic Basis for Computer Programming

  2013cited by this paper
• Automatic Inference of Access Permissions

  2012cited by this paper
• C++ AMP: Accelerated Massive Parallelism with Microsoft Visual C++

  2012cited by this paper
• A GPU-accelerated software eye tracking system

  2012cited by this paper
• GPUVerify: a verifier for GPU kernels

  2012influential reference
• GPU-based acoustical occlusion modeling with acoustical texture maps

  2011cited by this paper
• Barriers in Concurrent Separation Logic: Now With Tool Support!

  2011cited by this paper
• Scalable SMT-based verification of GPU kernel functions

  2010cited by this paper
• CUDA by Example: An Introduction to General-Purpose GPU Programming

  2010cited by this paper
• Verification of Concurrent Programs with Chalice

  2009cited by this paper
• Reasoning about Java's Reentrant Locks

  2008cited by this paper
• Accelerating advanced mri reconstructions on gpus

  2008cited by this paper
• Separation Logic Contracts for a Java-Like Language with Fork/Join

  2008cited by this paper
• Local Reasoning for Storable Locks and Threads

  2007cited by this paper
• Permission accounting in separation logic

  2005cited by this paper
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs

  2005cited by this paper
• Resources, Concurrency and Local Reasoning

  2004cited by this paper
• Checking Interference with Fractional Permissions

  2003cited by this paper
• Separation logic: a logic for shared mutable data structures

  2002cited by this paper
• Ten Years of Hoare's Logic: A Survey—Part I

  1981cited by this paper

• A Modular Static Cost Analysis for GPU Warp-Level Parallelism

  2026cites this paper
• Preserving provability over GPU program optimizations with annotation-aware transformations

  2025cites this paper
• Equivalence Checking of ML GPU Kernels

  2025cites this paper
• LLOR: Automated Repair of OpenMP Programs

  2024cites this paper
• Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs

  2024cites this paper
• Memory access protocols: certified data-race freedom for GPU kernels

  2023cites this paper
• GPURepair: Automated Repair of GPU Kernels (Extended Version)

  2023cites this paper
• Alpinist: An Annotation-Aware GPU Program Optimizer

  2022cites this paper
• Symbolic identification of shared memory based bank conflicts for GPUs

  2022cites this paper
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA

  2022cites this paper
• Automated Verification of the Parallel Bellman-Ford Algorithm

  2021cites this paper
• Checking Data-Race Freedom of GPU Kernels, Compositionally

  2021cites this paper
• A wearable sensor vest for social humanoid robots with GPGPU, IoT, and modular software architecture

  2020cites this paper
• GPURepair: Automated Repair of GPU Kernels

  2020cites this paper
• Behavioral Contracts for Cooperative Scheduling

  2020cites this paper
• Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms

  2020cites this paper
• Towards verified construction of correct and optimised GPU software

  2020cites this paper
• Theoretical Aspects of Computing – ICTAC 2020: 17th International Colloquium, Macau, China, November 30 – December 4, 2020, Proceedings

  2020cites this paper
• Integrated Formal Methods: 16th International Conference, IFM 2020, Lugano, Switzerland, November 16–20, 2020, Proceedings

  2020influential citation
• Formal Methods for GPGPU Programming: Is the Demand Met?

  2020cites this paper
• Formal Verification of Parallel Prefix Sum

  2020cites this paper
• NASA Formal Methods: 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings

  2020influential citation
• A survey on the use of access permission-based specifications for program verification

  2020cites this paper
• Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

  2019cites this paper
• Verification of GPU Program Optimizations in Lean by Björn Fischer

  2019cites this paper
• Access Permission-based Program Verification: A survey

  2019cites this paper
• Automatic Inference of Symbolic Permissions for Single-threaded Java Programs

  2019cites this paper
• Automatic Synchronization for GPU Kernels

  2018cites this paper
• Analysis of GPGPU Programs for Data-race and Barrier Divergence

  2018cites this paper
• Program Correctness by Transformation

  2018cites this paper
• Towards Reliable Concurrent Software

  2018cites this paper
• Verification of Program Parallelization

  2018cites this paper
• Formal analysis techniques for reliable GPU programming: current solutions and call to action

  2017cites this paper
• SafeGPU: Contract- and library-based GPGPU for object-oriented languages

  2017cites this paper
• A Hoare Logic for GPU Kernels

  2017cites this paper
• A Verification Technique for Deterministic Parallel Programs

  2017cites this paper
• Verifying spatial properties of array computations

  2017cites this paper
• The VerCors Tool Set: Verification of Parallel and Concurrent Software

  2017cites this paper
• Forward progress on GPU concurrency

  2017cites this paper
• A verification technique for deterministic parallel programs

  2017cites this paper
• Automated Verification of Functional Correctness of Race-Free GPU Programs

  2016cites this paper
• Implementing and Evaluating Candidate-Based Invariant Generation

  2016cites this paper
• Applying SPMD Verification Techniques to Hardware Description Languages

  2016cites this paper
• Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq

  2016influential citation
• Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq

  2015influential citation
• The Design and Implementation of a Verification Technique for GPU Kernels

  2015cites this paper
• Closer to Reliable Software: Verifying Functional Behaviour of Concurrent Programs

  2015cites this paper
• Optimization, Specification and Verification of the Prefix Sum Program in an OpenCL Environment

  2015influential citation
• Specification and Verification of Atomic Operations in GPGPU Programs

  2015cites this paper
• Verification of Loop Parallelisations

  2015cites this paper
• The VerCors Tool for Verification of Concurrent Programs

  2014cites this paper
• Verifying Parallel Loops with Separation Logic

  2014cites this paper
• Contract-based general-purpose GPU programming

  2014cites this paper
• Scalable verification techniques for data-parallel programs

  2014cites this paper
• Verification of Concurrent Systems with VerCors

  2014cites this paper
• Research Proposal NWO Open Competition 2014 1 Project data 1 a Project title

  year unknowncites this paper