Installing and Running VerCors

You can install VerCors by either using a release (recommended for beginners), or by building VerCors from its source code.

Using a Release

Installation

VerCors requires a java runtime environment (version 11 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-11-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.

Usage

VerCors verifies programs that are annotated with JML-style specifications (the underlying theory uses separation logic with permission accounting). Details on the specification language can be found on the VerCors Wiki pages. Furthermore, a large collection of example programs can be found (and verified) in the ./examples directory.

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 11 or greater, either OpenJDK or Oracle.
• Git (on Windows you need Git Bash, see https://git-scm.com/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 instructions for importing VerCors into either eclipse or IntelliJ IDEA here.

Running VerCors

VerCors verifies programs that are annotated with JML-style specifications (the underlying theory uses separation logic with permission accounting). Details on the specification language can be found on the VerCors Wiki pages. Furthermore, a large collection of example programs can be found (and verified) in the ./examples directory.

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

Syntax highlighting

When writing a program in PVL, the Prototypal Verification Language of VerCors, syntax highlighting can be obtained in the following way:

VerCors provides syntax highlighting support for PVL in TextMate 2 (MacOS X) and Sublime Text (Linux and Windows) as a TextMate Bundle. The bundle is located at ./util/VercorsPVL.tmbundle. On MacOS X for TextMate 2 you can simply double click the .tmbundle file to install it. Sublime Text requires you to copy the bundle content to some directory:

1. In Sublime Text, click on the Preferences > Browse Packages… menu.
2. Create a new directory and name it VercorsPVL.
3. Move the contents of VercorsPVL.tmbundle (that is, the ./Syntaxes directory) into the directory you just created.
4. Restart Sublime Text.

Visual Studio Code (VS Code) also has support for TextMate bundles to do syntax highlighting (VS Code runs on Windows, Linux and OSX). Click here for instructions on how to install this (this has not been tested however).