GMC – GIMPLE Model Checker for C/C++ programs


Jan Kouba kouba.honza<at-sign>
Ondrej Krč-Jediný ondro.krc<at-sign>
Jan Šebetovký jan<at-sign>
Ondřej Šerý ondrej.sery<at-sign>


David Hauzar hauzar<at-sign>
Jan Kofroň jan.kofron<at-sign>
Pavel Jančík pavel.jancik<at-sign>
Tomáš Poch poch<at-sign>

GMC is a part of the Ascens EU Integrated Project (IP) in the 7th Framework Programme (FP7):


GMC is an explicit-state code model checker for C/C++ programs. GMC is able to discover low-level programming errors such as buffer overflows, memory leaks, null-pointerdereferrence etc. GMC understands threads and executes all possible interleavings to discover errors manifested only in certain thread schedules. In particular, GMC understands the pthread library, but offers a means to extend the support for other thread libraries.

GMC's input is GIMPLE, the intermediate representation of the GNU Compiler Collection - GCC ( This architecture affords compatibility with majority of open source projects and easy interation into an existing make-based compilation toolchain.

In order to fight state explosion, GMC supports basic partial order reduction as well as incremental heap cannonicalization (based on paper M. Musuvathi and D. L. Dill: An Incremental Heap Canonicalization Algorithm).


GMC code is licensed under LGPL, with an exception of the GIMPLE export plugin for GCC which is licensed under GPL. Compilation instructions are in the source pack in the file INSTALL.

Type Version Link Description
GMC 0.5 gmc-0.5.tgz C support
GMC 0.9 gmc-0.9.tgz Current release


Jan Kouba Memory Representation for Model Checker of C/C++ Kouba-MemoryModel.pdf
Ondrej Krč-Jediný GIMPLE Model Checker KrcJediny-GimpleModelChecker.pdf
Jan Šebetovský Support for C++ in GMC Sebetovsky-C++Support.pdf
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>
  • How to find us?
Modified on 2016-02-11