GMC is an explicit model checker for the C and C++ languages. It is built upon the Gimplex++ representation of source code, an extension of the intermediate representation being used in the GCC project; the intermediate representation is called Gimple — that is where the GMC name stems from.

GMC is able to check the sources in C and the C++ language given that they do not contain calls to unsupported library functions. It supports verification of multi-threaded programs.

Even though support for POSIX threads is implemented, GMC provides general support for threading libraries, restricting the support incorporated to providing mapping of the thread functions (create thread, thread join, wait, ...) to the real function names in the form of a text file. GMC can verify that in any thread interleaving, no deadlock appears and no assertion stated in the code is violated.

Further Information:

• User Guide
• Download