cff-version: 1.2.0
abstract: "Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer) submitted to TACAS '22 conference. For a full description on how to use the artifact, please see the README.txt file. The artifact contains the Alpinist tool, all its dependencies and documentation for the VerCors tool.<br><br>Abstract of the paper:<br>GPU programs are widely used in industry. To obtain the best 
performance, a typical development process involves the manual or 
semi-automatic application of optimizations prior to compiling the code.
 To avoid the introduction of errors, we can augment GPU programs with 
(pre- and postcondition-style) annotations to capture functional 
properties. However, keeping these annotations correct when optimizing 
GPU programs is labor-intensive and error-prone.<br>This paper 
introduces Alpinist, an annotation-aware GPU program optimizer. It 
applies frequently-used GPU optimizations, but besides transforming 
code, it also transforms the annotations. We evaluate Alpinist, in 
combination with the VerCors program verifier, to automatically optimize
 a collection of verified programs and reverify them.  "
authors:
  - family-names: Şakar
    given-names: Ömer
    orcid: "https://orcid.org/0000-0003-3457-5446"
  - family-names: Safari
    given-names: Mohsen
  - family-names: Huisman
    given-names: Marieke
    orcid: "https://orcid.org/0000-0003-4467-072X"
  - family-names: Wijs
    given-names: Anton
title: "Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer)"
keywords:
version: 1
identifiers:
  - type: doi
    value: 10.4121/16938556.v1
license: Apache-2.0
date-released: 2021-11-22