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.

Pthread Model Checker automatically performs the following checks:

In addition, you can perform two types of assertion checks. One is general assertion defined in the standard header 'assert.h'. Another is called 'global assertion' which can monitor the values of global variables through the whole execution of a program. It is not needed to write down a detailed specification or write complicated temporal logic expressions. Pthread Model Checker automatically translates a model into a labelled transition system and checks the states exhaustively.

Pthread Model Checker performs checks in parallel. You can check large scale models fast by utilizing multicore CPUs and cloud computing power.

Please see the reference manual and related documents.

[*1] Recursive mutexes are not supported.
[*2] All threads must be PTHREAD_CREATE_JOINABLE.


How many threads can be used in checking 14Unlimied
Available Memory SizeLimitedUnlimitedUnlimied
Commercial UseNot permittedNot permittedPermitted
One-year License (without tax)3,000 JPY90,000 JPY

System Requirements

OS Linux, macOS (64 bit)*1
CPU Intel or AMD, x86_64 compatible processor
Memory 4 GiB or more*2
Storage at least 100 MiB
[*1] In the case of Microsoft Windows 10 (64bit), Linux version is available on Windows Subsystem for Linux (Bash on Windows).
[*2] The required memory depends on the size of a model.