« Previous - Version 10/24 (diff) - Next » - Current version
Stefan Blom, 03 Oct 2012 14:50


Overview

The VerCors project is about Verification of Concurrent Data Structures.

The VerCors toolset currently consists of two tools:

Binary Distribution

This chapter is about installing the binary version.

Prerequisites

To run the binary version, you will need a Java Runtime Environment. Note that the toolset has been tested with the Oracle Java 1.6 SE and 1.7 SE SDKs. Compatibility with other JVMs is untested.

Windows

The binary distribution requires no non-standard components.

Linux and MacOSX

The following two packages are needed:

  • wine (no known version requirements)
  • mono (2.10 or better)

Linux notes

  • All common Linux distributions include a package for wine, so it may be installed using the package manager of your distribution.
  • Not all common Linux distributions include a sufficiently up-to-date version of mono. Thus you may need to download sources from http://www.mono-project.com/ and follow instructions on how to compile them.

MacOSX notes

Unfortunately, we do not know of any binary distribution of wine on MacOSX. Thus, we recommend installing macports (http://www.macports.org/) and then installing wine:

sudo port install wine

For installing mono, you have two options:
  1. Get a binary distribution from http://www.mono-project.com/
  2. Install using macports:
    sudo port install mono???
    

Installation.

  1. Download the zip archive with the binary distribution. E.g. vct-1.0.zip.
  2. Extract the files from the zip archive.
  3. For easy command line access: add the bin subdirectory to your PATH variable.

Source Distribution.

The source distribution has been structured to allow both command line building with ant and development with eclipse.

Getting the sources.

There are two ways to get the sources:

  1. Download a zip archive.
  2. Clone one of the git repositories.

Git repository.

See Installing git for windows.

  • SSH based git server.

URL: :vercors-toolset.git
access: create an SSH key pair and email the public key to Stefan.

Note that the git repository has submodules. That is, after cloning one of the git repositories, you must initialize the sub modules:

git submodule update --init

Note that git does not automatically update submodules if you pull or check out a new version.
So further updates are likely to be needed.

Command line building.

Command line building uses Apache ant. To build the tool set go to the root directory and enter the command

ant

To create a distribution enter
ant dist

Overview of the Modules of the VerCors Tool set

The VerCors tool set is split into several modules plus scripts to make everything work together. You cannot use eclipse to manage the VerCors tool set. You can use eclipse to work on each module. For detailed configuration instructions for eclipse see Eclipse Setup.

Next, we will give an overview of the modules. The name of the subdirectory of the module is given between parenthesis.

Hybrid Runtime Environment (hre)

depends on: -

This module contains functionality that has uses outside of the VerCors toolset.

Core Data Structures (core)

depends on: hre

This module contains the main data structures for the VerCors toolset:
  • the Common Object Language (COL) Abstract Syntax Tree.
  • Pretty printing framework.
  • Visitor Patterns for AST.

Main program (main)

depends on: hre, core

The main program of the VerCors verifier Tool (vct).

Java Parser plugin (java-parser)

depends on: hre, core

Parser for Java, written with the JavaCC 5.0 parser generator.

To compile this parser plugin, you may:
  • Perform a command line build using ant.
  • Perform an eclipse build using the eclipse ant builder.
  • Install and use the JavaCC eclipse plugin.

PVL Parser plugin (pvl-parser)

depends on: hre, core

Parser for PVL (toy language used in the program verification course), written with the ANTLR 3.4 parser generator.

To compile this parser plugin, you may:
  • Perform a command line build using ant.
  • Perform an eclipse build using the eclipse ant builder.
  • Install and use the ANTLR v3 eclipse plugin.