SATABS Homepage Predicate Abstaction with SAT for ANSI-C

Eclipse Plugin for SATABS

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 SATABS, do the following:

  1. Install Eclipse. You must use location that does not contain spaces in the path name. Note that you need Eclipse 3.2. The version 3.1 will not work.
  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: "SATABS Plugin",
    URL Linux: http://www.cprover.org/satabs/plugin/lin/
    URL Windows: http://www.cprover.org/satabs/plugin/win/
    5. URL OSX/Intel: http://www.cprover.org/satabs/plugin/osx/
  5. Click "Finish"
  6. Select "org.feature.CProver", then click "Next"
  7. Read and accept the license (by clicking "Next"), then click on "Finish"
  8. There will be a warning that the code is not digitally signed. Click "Install".

To use the plugin:

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

The SATABS Manual contains more information about the plugin.