Over the years, I have developed a number of software tools for scientific purposes. In time, these will be made publicly available via this webpage.

Extensions of Existing Tools

The following are extensions developed by me of existing tools developed by other people:

  • The μCRL toolset 2.18.5 extended with:
    • support for (modelled) absolute time stamps;
    • an implementation of a partial order reduction technique for branching security protocol specifications;
    • an implementation of priority beam search.
    •      		DOWNLOAD
  • GPU-PRISM: PRISM with support for NVIDIA General Purpose Graphics Processing Units;
    •      		DOWNLOAD
    INSTRUCTIONS
  • LTSmin-hive: The LTSmin toolset extended with support for HIVE, to perform informed swarm verification (client side).
    •

    New Tools

    The following are tools completely developed by me.

    GPU-Accelerated Model Checking Tools

    I am working on a toolset for (so far explicit-state) model checking of concurrent system models by means of General Purpose Graphics Processing Units (GPGPUs). To run, the toolset requires a computer equipped with an NVIDIA GPGPU. For some tools, at least CUDA computing capability 2.0 or 3.0 is required.

  • GPUexplore: for on-the-fly state space exploration.
    		• TOOL WEBPAGE
  • GPUdecompose: to decompose directed graphs into Strongly Connected Components, and graphs underlying Markov-Decision Processes into Maximal End Components.
    		• RELEASED SOON

    Distributed Model Checking Tools

  • HIVE: for informed swarm verification (manager side).

    • Verifying Model Transformations and Compositional Model Checking

    Other research I'm working on involves formally verifying the functional property preservation of behavioural model transformations, and the compositional model checking of concurrent system designs.

  • REFINER: First of all, formally specifying behavioural transformations of concurrent system models, applying such transformations, and verifying that they preserve specific functional system properties. Such properties can be safety and liveness properties. Second of all, compositionally verifying that a concurrent system model satisfies a regular safety property. This involves a novel technique called Incremental Counter-Example Construction (ICC).
    		• TOOL WEBPAGE