PuMoC

A CTL Model Checker for Sequential Programs

Home

Download

Quick Start

References

Experiments

 

 

 

PuMoC has been tested mainly on Linux distributions and Windows Cygwin.

Downloads:

Source code for PuMoC

PuMoC is implemented in C programming language.

 

Tips for installing PuMoC on Linux or Cygwin.

Download the source code for PuMoC, first install the cudd library using the following commands. PuMoC is equiped with cudd-2.4.2. Up-to-date versions can be obtained from the CU Decision Diagram Package .

tar -zxvf PuMoC.tar.gz

cd PuMoC/cudd-2.4.2

make

Copy object files libcudd.a, libepd.a, libmtr.a, libst.a, libutil.a from the directory cudd, epd, mtr, st, util to the directory lib in cudd-2.4.2 by the following commands:

cp -i cudd/libcudd.a lib/

cp -i epd/libepd.a lib/

cp -i mtr/libmtr.a lib/

cp -i st/libst.a lib/

cp -i util/libutil.a lib/

Now, you can install PuMoC by the commands:

cd..

make

Now, you can evaluate an example: ./PuMoC -l2 test/quick start.abpds.

Here -l2 specifies checking the emptiness of the alternating Buechi pushdown system quick start.abpds.

 

Copyright © 2011-2012 LIAFA, University of Paris Diderot and CNRS.