Contact Us Publications Case Studies Manual Home

CCMC Tool Homepage

CCMC is a probabilistic model checker for the model checking of Continuous Stochastic Logic [CSL (aziz2000model)] and Conditional CSL Logic [CCSL (gao2012model)] over continous-time Markov chains (CTMCs). CCMC provides an interface to parse the output files of PRISM. This way, the user can model a CTMC model with PRISM, and then use the output model files of PRISM as the input of CCMC. To improve efficiency, in CCMC the stratification method [zhang2011automata, gao2012model ] is used to preprocess the CTMC model.The CCMC source code is available under the GNU General Public License (GPL) Version 3.

Download and Installation

The latest binary and source code of CCMC 1.1 can be obtained below.



For earlier versions (Not stable!)


To compile and install CCMC by yourself, the following is required:


Once you have decompressed the source package, change to the ccmc-1.x directory. Then run the configure script and compile the tool.

$ ./configure LDFLAGS="-L<gsl_lib_path>" CPPFLAGS="-I<gsl_include_path>" 
$ make

You can use some other options by typing:

$ ./configure --help


You can install CCMC as follows:

$ sudo make install

By default, ccmc will be installed in '/usr/local/bin' and manpage will be installed in '/usr/local/share/man/man1'. If you want to change this, you can set the prefix when you run './configure'.

In case of problems with running the binary or compiling the sources, please contact Yang Gao (


CCMC was developed by Yang Gao, Naijun Zhan, and Lijun Zhang.


For questions, comments and support requests regarding CCMC, please contact Yang Gao (, Naijun Zhan (, or Lijun Zhang ( .