Overview

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 (gcc.gnu.org). 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).

Authors

  • Jan Kouba
  • Ondrej Krč-Jediný
  • Ondřej Šerý

Contributors

  • David Hauzar
  • Pavel Jančík
  • Jan Kofroň
  • Tomáš Poch