CProver based model checking with Auto FOCUS 3

Introduction

AF3 provides a integration of the CProver model checkers CBMC and SATABS with the following features:

Installing CProver

To use the CProver model checking functionality in AF3, firstly we have to install the CBMC and/or SATABS model checkers (download can be found here for CBMC and here for SATABS).

For Linux and MasOS:

You only have to make sure that CBMC and/or SATABS is in the PATH.

For Windows:

1.    Make sure, that the folders in which your CBMC and/or SATABS binary files are contained in, are in the Path environment variable.

2.    All CProver model checkers require to be able to access a c compiler, thus you have to make sure a compiler is available. AF3 provides support for Cygwin (with gcc installed) or Microsoft Visual Studio (Visual Studio Express is sufficient).

For Cygwin, make sure that Cygwin's bin folder is in the Path environment variable.

For Visual Studio, add the folder which contains VsDevCmd.bat to the Path environment variable. Usually, this is something like C:\Program Files\Microsoft Visual Studio 11.0\Common7\Tools.

To check whether AF3 can access CBMC and/or SATABS, just press the "CProver Version" button from the "CProver Analyses View". If CBMC and/or SATABS are correctly installed, a dialog showing its version is displayed (as below), otherwise an error message will be displayed.


Using the "Semantic Inspector"