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
are symbolic tools for infinite-state model checking.
They operate on linear process specifications
(LPSs) and parameterised Boolean equation systems
solves PBESs through instantiation, but tries to reduce the underlying graph by applying partial-order reduction