« Previous - Version 15/24 (diff) - Next » - Current version
Stefan Blom, 12 Feb 2013 14:17


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

You need mono, version 2.10 or better, to run Boogie.

  • 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.
  • For installing mono, you have many options. For example:
    1. Get a binary distribution from http://www.mono-project.com/.
    2. Get the sources from http://www.mono-project.com/ and install them.
    3. 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.

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

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

git submodule update --init

and after every update, you must synchronize
the submodules:
git submodule sync
git submodule update

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. The idea behind the modules is that you can choose between command line and eclipse development for each module independently. 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, clang

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.

CLang Parser plugin (clang-parser)

depends on: hre, core

Parser for C, C++, etc. using the clang/llvm parser.

To compile this parser plugin, you will need to:
  • Install clang+llvm version 3.2.
  • Configure eclipse to compile this projects.