PuMoC

A CTL Model Checker for Sequential Programs

PuMoC is a CTL model checker for pushdown systems (PDS), and sequential C/C++ and Java programs.

The CTL model checking problem for PDSs is reduced to the emptiness problem of alternating Buechi pushdown systems.

PuMoC allows to check CTL properties for PDSs w.r.t. simple valuations, where the atomic propositions depend on the control locations of the PDSs, and w.r.t. regular valuations, where atomic propositions are regular predicates over the stack content.

PuMoC allows also to do CTL model checking for sequential boolean, C/C++ and Java programs. Indeed, sequential boolean programs can naturally be modeled by PDSs. To translate C/C++ sequential programs into boolean programs, we use Satabs , whereas to extract a PDS from a Java program, we use JimpleToPDSolver.

In addition to CTL model checking, PuMoC is intergrated with Moped. This offers a toolkit that can do both LTL and CTL model-checking for PDSs and sequential programs.

Given a CTL formula and an input file (boolean programs, pushdown systems), or an alternating pushdown system, PuMoC either outputs Yes or No when the input file has an initial configuration, otherwise PuMoC outputs a finite automaton (FA) recognizing all the configurations which satisfy the CTL formula.

Contact: PuMoC is written and maintained by Fu Song.

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