Projects

Tools

Below is a short description of the formal methods 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 pbessymbolicbisim are 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. Furthermore, I have also made significant improvements to the tools lpsparunfold and pbesconstelm.

COAL

This tool for COmpositional Automata Learning is build on top of LearnLib and implements a compositional algorithm for learning large transitions systems in the style of L*. These ideas are described in a FASE paper, a reproduction package (including the sources) is available on Zenodo.

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.