« Previous - Version 5/24 (diff) - Next » - Current version
Stefan Blom, 19 Jul 2012 13:56


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 SDK.
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 repositories.
  • EWI compute server demeter.

URL: demeter.ewi.utwente.nl:/home/sccblom/git/vercors-toolset.git
access: UTwente AD password, you can setup key logins if you like. This repository is read-only, to upload changes you need to create you own repository.

  • Temporary SSH based git server.

URL: :vercors-toolset.git
access: create an SSH key pair and email the public key to Stefan. This repository is read/write.

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

git submodule update --init

Command line building.

Command line building uses Apache ant.
To build the toolset got to the root directory and enter the command

ant

To create a distribution enter
ant dist

Setting up for eclipse development.

The VerCors tool set is split into several modules, which have to be configured as eclipse projects.

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.