You may find in this page the information on the verification software that I (co-)authored. They involve model-based runtime verification, test generation, game-based diagnosis for concurrent system design, and automatic verification techinques such as model checking, equivalence checking, and preorder checking. Click buttons on the left side for the information about each individual software.

Copyright notice: please check the license agreement included in the distribution of each software. You must agree the terms of its license agreement before using the software. In general, these software are free for academic use, and available either in the executable or the source code, or sometimes both.

CWB-NC is an intergreted verification package, which supports several automatic techinque techinques including model checking, equivalence checking, and preordering checking.

PlayGame is a game-based tool for debugging concurrent system designs. PlayGame allows the user to investigate a system design and understand the verification result by playing games with the computer. It support mu-Calculus model checking, and a variety of equivalence checkings and preorder checkings.

M²IST is a toolkit for supporting model-based runtime verification. It includes a model instrumentator, which prepares an embedded system design for runtime verification, and a monitor synthesizer, which generates a model-based runtime checker from the temporal-logic system requirement.

CHARONTESTER is a simulation-based test suite generator for hybrid systems.