Ludwig-Maximilians-Universität München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

CMC model checker

CMC is model checker implemented in component technology. It is intended to be a showcase for high-performance component technology.

Currently, this page is a mere placeholder. It will be extended once a stable version is reached. In the meantime, take a look at the measurements (a loose assembly of various experiments, some of them outdated).

Download

You can get an alpha version here. Make sure to read the README file.

Publication

The algorithm and some measurements are described in
  • Moritz Hammer and Michael Weber. "To Store or not to Store" Reloaded: Reclaiming Memory on Demand. FMICS. Springer, 2006.

    • Related projects

    Currently, there is one component for the creation of states, which utilizes the NIPS Promela virtual machine by Michael Weber.

    For disk-based model checking, we use the zlib by Jean-loup Gailly and Mark Adler.

    Moritz Hammer, Mar 06, 2006