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 fundamental improvements to the tools lpsparunfold and pbesconstelm.

CoalA

This tool for COmpositional Automata Learning with Alphabet refinement is build on top of LearnLib and implements a compositional algorithm for learning large transitions systems from a black box system in the style of L*. The embedded parallel components are discovered automatically using our alphabet refinement algorithm described in our CONCUR paper. A reproduction package (including sources) is available on Zenodo. The first version of this tool was called Coal (paper, artefact). It does not yet include the techniques for automatically finding the component alphabets, instead relying on user input.

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.