CegarMC: Integrating CEGAR Model Checking into a C Verification Framework

Overview

CegarMC is a tool that allows for CEGAR model checking within the Frama-C framework for analysis and verification of C programs. CegarMC is implemented as a Frama-C plugin (GUI version only) and allows for the verification of statement contracts. It is intended to be used together with other Frama-C plugins especially including those for abstract interpretation (value analysis) and deductive verification (wp).

Please report any bugs/comments to Subash Shankar (subash.shankar12@hu34nter.cuny.edu with the digits removed). We would also love to hear of any applications you may be using the tool on.

Installation Instructions (Linux/Mac only)

These instructions include the versions of the tools that CegarMC has been tested/developed with, though It will probably also work with other versions except as otherwise stated. You may skip step 2 or 3 if you wish to use only 1 back-end CEGAR tool, though it is recommended that you install both since they won't generally work on the same programs.

  1. Install frama-c (Chlorine) from source. Note that cegarMC is not compatible with the standard yum bundle; thus, the need for a source build. 
  2. Install satabs (3.2).
  3. Install CPAChecker (1.7). 
  4. Set your $CPACHECKER environment variable (e.g., to /opt/cpachecker). Make sure that satabs (and the associated files boom, goto-instrument, goto-cc) are in your path.
  5. Download and unpack cegarMC.
  6. Make sure that cegarmc.ml and mc-helper.sh are in the same directory (and in your path, if not in $PWD)

To test that everything has been installed properly type:

  1. frama-c-gui -load-script cegarmc.ml -mc -mc-checker satabs <prog.c> on a program with a statement contract to be verified.
  2. Select the statement contract (right-click on "\*@" is one way) , and select "Prove contract using MC" on the popup menu.
  3. CegarMC should then attempt to verify the statement contract.
  4. Repeat the above using the "-mc-checker cpa" option.

Usage Instructions

CegarMC allows for the verification of statement contracts expressed using a subset of ACSL constructs.The options are:

Option
-mc
 enable cegarmc plugin
-mc-help
 this list
-mc-checker {cpa,satabs}
 CEGAR model checker backend
-mc-output <filename>
 Name of intermediate file (will be overwritten)
-mc-context
 Use value analysis to assume initial values for variables in statement (ignored if -val flag is not used)
-mc-maxcontext <n>
 The number of values to enumerate in the context. If it is unable to determine a context that has fewer than n values, an interval is used. Note that large values of n may adversely affect CEGAR performance since it can also be used to generate more predicates for abstraction
-mc-numiter <n>
 The number of CEGAR iterations (not supported with cpachecker)
-mc-timelimit <n>
 Timeout (in seconds) for CEGAR checker