« Previous - Version 16/24 (diff) - Next » - Current version
Stefan Blom, 08 Apr 2013 13:51


Overview

The VerCors project is about Verification of Concurrent Data Structures.

The VerCors toolset currently consists of two tools:

Online Demo

Several verified examples are available in the online version of the verifier .

Prerequisites for the distributions.

To run the tools, you will need a Java 7 Runtime Environment. Note that the toolset has been tested with the Oracle Java 1.7 SE SDK. Compatibility with other JVMs is untested.

Windows

The tool distribution requires no non-standard components.

Linux

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

Note that, 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.

Mac OS X

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

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???
      

Binary Distribution

Obtaining the code

There is no public release yet. Please ask for a copy by email.

Installation

  1. Given 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 Blom.
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.