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.