Scalable Verification Techniques for Data-Parallel Programs: Accompanying Artifact
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
fig2.2
fig2.3--4
fig2.5
fig2.6
fig2.7
fig2.8
fig3.1
fig3.3
fig3.6
fig3.7
fig3.8
fig4.1
fig4.4
README

README

Scalable Verification Techniques for Data-Parallel Programs
===========================================================

We give code for each of the figures appearing in the thesis. These are either
Boogie, CUDA or OpenCL applications. The code for each figure is found in its
matching directory.

Contact
=======

Nathan Chong <nathan.chong@gmail.com>

Prerequisites
=============

The CUDA application (fig 2.2) requires a platform with the NVIDIA CUDA toolkit.
The OpenCL application (fig 2.3 and 2.4) requires a platform with an OpenCL
implementation. The Houdini example (fig 3.3) requires a local install of
Boogie. All other examples can run using the rise4fun web interfaces for
Boogie or GPUVerify.

  http://rise4fun.com/Boogie
  http://rise4fun.com/gpuverify-cuda
  http://rise4fun.com/gpuverify-opencl

Instructions for installing Boogie and GPUVerify locally are online.

  https://boogie.codeplex.com
  http://multicore.doc.ic.ac.uk/tools/GPUVerify/