Model Checking on Accelerators

title:Model Checking on Accelerators
keywords:High-performance computing, model checking, accelerators
topics:Dependability, security and performance
contact:W.H.M. Oortwijn MSc & prof.dr. M. Huisman


There is a lot of ongoing research on parallel model checking [1], distributed model checking [2], and on model checking with GPUs [3]. Some of this research also focusses on a certain combination of these approaches, for example by proposing model checking algorithms that are both parallel and distributed [2].

This research project focusses on combining parallel/distributed model checking with accelerator programming, targetting GPUs or Xeon Phi's. You will investigate scalable data structures that allow accelerators to be involved in the model checking problem, and you will make a proposal for this. You are expected to implement some of these data structures for GPUs or Xeon Phi's and experimentally demonstrate that the implementation is scalable.


  1. LTSmin: High-Performance Language-Independent
  2. Distributed Symbolic Reachability Analysis
  3. Many-Core On-The-Fly Model Checking of Safety Properties Using GPUs