Contractor Validation Tool

 
 

The Contractor tool has been developed using Python and has been tested to work successfully on Windows, Linux and Mac OS X platforms.



Contractor 0.41 (March 2010)

The Contractor tool is distributed under the GNU General Public License Version 3 (29 June 2007).

 

Get the Contractor tool

In order to install the Contractor tool in your system, make sure that the Python interpreter is installed.

If abstractions are to be produced using C source code as input, then:

  1. BulletMake sure that the Blast software model-checker is installed. The path to the Blast executable can be set using:

  2. contractor --blast-path=/path/to/blast-executable input-file


If abstractions are to be produced using contracts as input, then:

  1. BulletMake sure that CVC3 is installed. The path to the CVC3 executable can be set using:

  2. contractor --cvc3-path=/path/to/cvc3-executable input-file


  3. BulletOptionally, check that Yices is installed. In order to use Yices as a prover use:

  4. contractor -p yices --yices-path=/path/to/yices-executable

        --cvc3-path=/path/to/cvc3-executable input-file


  5. (Note that CVC3 is still required when using the Yices prover)

Optionally, in order to produce models directly in PDF or PNG formats:

  1. BulletCheck that Graphviz is installed. The path to the Dot executable can be set using:

  2. contractor --dot-path=/path/to/dot-executable input-file


When these requirements are met, you can run Contractor by executing the “contractor” file included in the ZIP file. Alternatively, you can run the Python interpreter passing “contractor” as the first argument.

 

Install the Contractor tool

If you would like to download a previous version of Contractor, go ahead but we won’t be able to provide you any support.

  1. BulletContractor 0.30 (August 2009)

  2. BulletContractor 0.10a (December 2008)


All of the Contractor versions are distributed under the GNU General Public License Version 3 (29 June 2007).

Archive: unsupported versions