ProductsDocumentationsAbout Us

Pthread Model Checker

Pthread Model Checker is a model checking tool for multithreaded programs with POSIX thread (pthread). Using it, you can detect problems which could be difficult to find by testing, such as deadlocks and livelocks.

You can write models in the programming language C (a subset). You need not study yet another modeling language.

SSG: A Parallel Refinement Checker

SSG is a tool to check the correctness of programs. You can check the correctness of large-scale programs in parallel by utilizing multicore CPUs and cloud power. SSG strongly supports the development of high-quality software by detecting problems which might be overlooked with tests.

For more information, please visit this page.

MCCSP: A CSP Communication Library for C/C++

MCCSP is a CSP communication library for C/C++. Using SSG, you can implement design models checked with SyncStitch or SSG in the same CSP style consistently. This consistency can reduce the possibility to make bugs in the implementation phase. It also makes it easier to maintain source code because the correspondence and the tracability between the models and the source code are clear.

MCCSP has simple interfaces. It can easily be used for the existing systems without modifying the thread design or the class design of the systems. There is no conflict in classes of the existing code and the library as often seen in other class libraries.

MCCSP is royalty-free. The source code is bundled. You can adjust it to the target systems. For more information, please visit this page.

SyncStitch: A Tool for Designing Concurrent Systems

SyncStitch is a tool that assists software professionals to design software systems. You can describe the behavior of target systems and their components as models and check whether they behave as you expect or not. SyncStitch is based on the CSP theory (Communicating Sequential Processes).

Please see this page for more information.


8 October 2017 Pthread Model Checker is released.
1 July 2017 SSG is released.
1 July 2017 MCCSP is released.
26 November 2016 We have formally proved one of the most important theorem in theoretical CSP "the congruence between operational semantics and denotational semantics on traces" by using the theorem prover Isabelle/HOL. We reported this achievement at the 18th society for the study of CSP held at TOYO University. You can access the outline of the proof here.
19 November 2016 Gave an introductory presentation about CSP at the Static Code Analysis meeting. You can download the material from here.
30 November 2014 Gave a presentation about "A Reduced Modeling Language and Its Processing for Efficient CSP Refinement Checking" at the 16th society for the study of CSP held at TOYO University. The presentation material is here.
6 June 2015 Reported libraries for concurrent programming in C based on CSP at the 15th society for the study of CSP held at TOYO University. The presentation material is here.
18 April 2015 SyncStitich version 1.2.0 is released.
30 November 2014 Reported preliminary result of applying parallel and on-the-fly methods to CSP refinement checking at the 14th society for the study of CSP held at TOYO University. The presentation material is here.
4 September 2013 SyncStitich version 1.1.1 is released.
26 August 2013 SyncStitich version 1.1.0 is released.
29 July 2013 Developers Blog "Think Stitch" is started.
23 July 2013 SyncStitch is released.