MACHINAIDE: Knowledge-based services for and optimization of machines, Faculty Participant (2022)
CLeVer: Verification of Hardware Concurrency via Model Learning, Postdoctoral Research Assistant (2020-2021)
Below is a short description of the academic tools I work on or have worked on.
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
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.
For my master
thesis, I have improved the GPU model checking tool
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.