CBMC Homepage Bounded Model Checking for ANSI-C

Eclipse Plugin for CBMC

Requirements:

  1. Windows: You need Visual Studio (as preprocessor). The Visual Studio executables need to be in the PATH environment variable.
  2. Linux: You need gcc and the usual header files.

To download and install the Eclipse plugin for CBMC, do the following:

  1. Install Eclipse, version 3.2. You must install it into some location that does not contain spaces in the path name. The plugin does not work with Eclipse version 3.1.
  2. Start Eclipse, open "Help" → "Software Updades" → "Find and Install"
  3. Select "Search for new features to install", then "Next"
  4. Click "New remote site", Name: "CBMC Plugin",
    URL Linux: http://www.verify.ethz.ch/satabs/plugin/lin/
    URL Windows: http://www.verify.ethz.ch/satabs/plugin/win/
    URL Mac OS X: http://www.verify.ethz.ch/satabs/plugin/osx/
  5. Select the "CBMC Plugin", klick "Finish"
  6. Select "org.feature.CProver"
  7. Read and accept license, then "Finish"

To use the plugin:

  1. Click "New" → "Project" → "CProver" → "New Verification Project"
  2. Select the new project
  3. Clock "New" → "New Task"
  4. Double-click the task
  5. "Files" tab: choose the files to model check
  6. "Options" tab: various options for running CBMC/Satabs
  7. Create a new CPROVER launch configuration using the green run button.
  8. After running CBMC, the claims for the selected task are displayed in the "Claims" view.
  9. Click on "Check All" in the "Claims" view to run the model checker
  10. If a counterexample is produced for a claim, click on the claim to step through the trace.