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