author: Danny Bergsma
title: Specification and verification of a compression algorithm in a GPU
keywords: gpu programming, verification, compression algorithm
topics: Algorithms and Data Structures
committee: Saeed Darabi ,
Marieke Huisman
started: July 2017


Exploring states using a scalable algorithm is one of the performance issues that any model checker can benefit. One of the core components in these algorithms is an efficient and reliable mechanism to handle state vectors. To achive this it is recommended to employ a provably correct compression algorithm.

On the other hand GPU's are increasingly used for general purpose computing, they can beat CPU performance by several orders of magnitude for some problems. GPU's offer huge level of parallelism running hundreds of threads in a lock step and it's special memory model allows it to reduce time to access memory while performing intense calculations.

To achieve higher scalability and performance the algorithm can take advantages of GPUs. Currently a multi-core tree-based state vector compression algorithm is proposed by FMT group [1] and implemented in LTSmin. The project aims to implement and verify the algorithm using GPU programming technology.


+ Study the literature

+ Define lockless hashtable data structure in GPU

+ Define compression tree data structure in GPU

+ Implement compression algorithm in GPU

+ Specify the algorithm using the specification language

+ Prove the implementation with respect to the specification



  1. Alfons Laarman, Jaco van de Pol, Michael Weber: Parallel Recursive State Compression for Free. SPIN 2011: 38-56 (Digital version available here)
  2. Khronos OpenCLWorking Group. The OpenCL Specification, version 1.2, 2001, URL (Digital version available here)
  3. J. Tompson, K. Schlachter. An Introduction to the OpenCL Programming Model. (Digital version available here)