Installing and Running VerCors

Using a Release

Installation

VerCors requires a java runtime environment (version 8 or later), as well as clang if you want support for C.

Linux

Currently we support debian-based systems; let us know if you need something else! Install the dependencies:

sudo apt install clang openjdk-8-jre 

Obtain the latest deb release of VerCors here, and install it by running:

sudo dpkg -i Vercors_x.y.z_all.deb

Mac

You can for example obtain the dependencies through homebrew:

brew cask install java

This should install the latest release of OpenJDK. Clang should already be installed through XCode.

Obtain the latest zip release of VerCors here and unzip it. You can find the run script for VerCors in the bin subdirectory.

Windows

You can obtain a java runtime environment e.g. here. Make sure that the environment variable JAVA_HOME points to wherever you unpack the JDK. clang can be obtained as part of the llvm toolchain here. Make sure that clang is added to the path.

Next, download the latest zip release of VerCors here and unzip it. You can find the batch script for VerCors in the bin subdirectory.

Running VerCors

The VerCors toolset can be used by running vercors --silicon <filepath>, with <filepath> the path of the (Java, C, or PVL) file to verify.

Building from source code

Installation

When building VerCors, you additionally need these dependencies:

• A Java Development Kit, version 8 or greater, either OpenJDK or Oracle.
• Git (on Windows you need Git Bash, see https://git-scm.com/downloads)
• Mercurial (See https://www.mercurial-scm.org/downloads)
• Scala SBT, version 1.3.0 or greater (see http://www.scala-sbt.org for instructions)

1. Clone the VerCors repository using git clone https://github.com/utwente-fmt/vercors.git and move into the cloned directory, cd vercors.
2. Run sbt compile to compile VerCors.
3. Test whether the build was successful by running ./bin/vct --test=examples/manual --tool=silicon --lang=pvl,java --progress.

The last command tests the VerCors installation by verifying a large collection of examples (from the ./examples directory). This command should eventually report that all ? tests passed. There are also intstructions for importing VerCors into either eclipse or IntelliJ IDEA here.

Running VerCors

The VerCors toolset can be used by running ./bin/vct --silicon <filepath>, with <filepath> the path of the (Java, C, or PVL) file to verify.