Projects

Tools

Below is a short description of the academic tools I work on or have worked on.

mCRL2

mCRL2 is a toolset for model checking concurrent processes. Models are specified in the mCRL2 process algebra; formal properties can be formulated in the modal mu-calculus. I have worked on several ways to improve the underlying algorithms for model checking. The tools I have developed are lpssymbolicbisim, pbessymbolicbisim and pbespor. lpssymbolicbisim and pbessymbolicbisimare symbolic tools for infinite-state model checking. They operate on linear process specifications (LPSs) and parameterised Boolean equation systems (PBESs), respectively. pbespor solves PBESs through instantiation, but tries to reduce the underlying graph by applying partial-order reduction.

GPUexplore

For my master thesis, I have improved the GPU model checking tool GPUexplore. I added partial-order reduction to improve the memory efficiency and improved the speed with a factor 11 over the previous version. This brought the total speed-up over a single-threaded implementation to well over a hundred times. The thesis has been awarded with the Ngi-NGN Informatie Scriptieprijs (second prize) in 2016 and was nominated for the ENIAC best thesis award.