PuMoC

A CTL Model Checker for Sequential Programs

Experiments on an extensive set of benchmarks are given below. The benchmarks are:

1. Verifying Random Pushdown Systems;
2. Verifying 1461 versions of 30 real-world Windows Drivers taken from SLAM benchmarks;
3. Model checking C and Java Programs where C source codes taken from a bounded model checkers verds, Java source codes of JimpleToPDSolver, SciMark2 and JBDD;
4. Data flow analysis of Java Programs taken from PDSolver.

All the tests were run on a Fedora 13 with a 2.4GHz CPU and 2GB of memory.

1. Verifying Random Pushdown Systems.

We randomly generated 500 PDSs each of them equipped with a random CTL formula. The number n of control locations and stack alphabet ranges from 10 to 510. The number of transition rules ranges from n2 to 2n2. The size of the CTL formulas ranges from 2 to 15. Figure (a) depicts the time consumption w.r.t. the size n. Only 5:2% (i.e., 26) of the cases run out of time (30 minutes) while the majority of cases terminated in a few seconds. Figure (b) depicts the memory consumption w.r.t. the size n. Only 6:6% (i.e., 33) of tests run out of memory with 2GB limitation. The majority of tests finished in a few MB. This benchmark includes 500 pushdown systems can be download [here].

Figure (a): On Time Performance	Figure (b): On Memory Performance

2. VerifyingWindows Drivers.

We tested 1461 versions of 30 real-world drivers. All these versions are taken from SLAM benchmarks. SLAM provides the boolean programs corresponding to these drivers.We checked 2 CTL formulas that are relevant for these drivers. The first formula r1 ensures that the programmer uses the API functions in the good order. This formula uses regular valuations to ensure that whenever a function named DeviceAdd is called, the function DeviceCreate will be called eventually before DeviceAdd returns. The second CTL formula r2 describes a locking property. Our results are described in Table 1. Column No. Versions gives the number of versions we considered of the corresponding driver. Column Avg. #LOC denotes the average size of the programs’ versions. Column Avg. Time(s) and Avg. Mem(MB) give the average time and memory in seconds and MB.

Table 1. Model-Checking Drivers with PuMoC

3. Model checking C and Java Programs.

We also were able to check several CTL properties of several C and Java programs. We checked the C source code of a bounded model checker (verds). We also checked 4 real-world Java programs taken from JimpleToPDSolver, 4 real-world Java programs taken from a Java benchmark SciMark2 , and 7 real-world Java programs taken from JBDD . The experimental results are summarized in Table 2.

Table 2. Checking C and Java programs with PuMoC

4. Data flow analysis of Java Programs.

PuMoC can also perform Data Flow Analysis of Java programs. Given a Java program, JimpletoPDSolver translates it into a PDS with def/use informations, where the atomic proposition de f (x) (resp. use(x)) of a variable x holds at a control point if its corresponding statement is an assignment (resp. a use) of the variable x. Using these informations, we can write CTL formulas that can solve some data flow analysis problems like reaching definitions, live variables, very busy expressions, and available expressions. For example the formula E[!de f (x)U use(x)] checks whether the variable x is used ithout being defined. This allows to do live variables analysis. Similarly, the formula AG(de f (x) => EF use(x)) states that whenever the variable x is defined, it should be used in some path. Checking such property allows to optimize programs. Indeed, the variable x does not need to be defined if x will not is used. Table 3 summarizes the results of our experiments. We made a comparision with PDSolver, a mu-calculus modelchecker for PDSs and Java programs (CTL formulas can be translated to mu-calculus). Our tool is more efficient.

Table 3. Data flow analysis of Java Programs with PuMoC

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