This repository hosts VerCors, a toolset for the verification of concurrent and parallel programs. VerCors aims to verify many different concurrency constructs, including: heterogeneous concurrency (Java and C), GPU kernels using barriers and atomics (OpenCL), and compiler directives as used in deterministic parallelism (OpenMP). VerCors is able to prove data-race freedom, memory safety, and functional correctness of (concurrent) programs written in Java, C, OpenCL, OpenMP, and PVL (Prototypal Verification Language, a procedural toy language for prototyping new verification features). Moreover, VerCors is designed to be language-independent, which makes adding new front-end languages a straightforward engineering effort.
A list of verified examples and case studies is maintained online and can be found here. This webpage also contains an online interface for VerCors and allows you to try VerCors online.
VerCors requires a java runtime environment (version 8 or later), as well as clang if you want support for C.
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.debYou can for example obtain the dependencies through homebrew:
brew cask install javaThis 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.
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.
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.
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)
- Scala SBT, version 1.3.0 or greater (see http://www.scala-sbt.org for instructions)
- Clone the VerCors repository using
git clone https://github.com/utwente-fmt/vercors.gitand move into the cloned directory,cd vercors. - Run
sbt compileto compile VerCors. - 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.
- For questions and support, email to [email protected].
- For bug reports and feature requests, visit https://github.com/utwente-fmt/vercors/issues.
A complete list of papers on the VerCors project is given here.
Copyright (c) 2008 - 2019 Formal Methods and Tools, University of Twente All rights reserved.
The license to VerCors is a mozilla open source license as described in LICENSE.TXT in the root of this project. It is a free to use, share-alike license. Should this license be too restrictive for your purpose, please let us know by creating an issue in our bug tracker. Direct contributors (people who send us pull-requests or edit this repository directly) are expected to agree with any license that the University of Twente might decide. If you do not agree with future license changes, please instead fork this repository as allowed under the conditions of LICENSE.TXT.