README.md

November 16, 2024 · View on GitHub

This is ViperServer, an HTTP server that manages verification requests to different tools from the Viper tool stack.

The main two Viper tools (a.k.a verification backends) currently are:

Carbon, a verification condition generation (VCG) backend for the Viper language.
Silicon, a symbolic execution verification backend.

Viper IDE: integration of Viper into Visual Studio Code (VS Code). Viper IDE provides the best user experience for Viper. More details here: http://viper.ethz.ch/downloads/
Facilitate the development of verification IDEs for Viper frontends, such as:
- Gobra, the Viper-based verifier for the Go language
- Prusti, the Viper-based verifier for the Rust language
Avoid 1-3 second delays caused by JVM startup time. ViperServer offers a robust alternative to, e.g., Nailgun.
Develop Viper encodings more efficiently with caching.
Interact with Viper tools programmatically using the HTTP API. A reference client implementation (in Python) is available via viper_client.

For more details about using Viper, please visit: http://viper.ethz.ch/downloads/

Clone viperserver (this repository) in your computer.
Execute git submodule update --init --recursive in the cloned directory to fetch the carbon, silicon, and (transitively) the silver repositories. Note that both carbon and silicon have a silver submodule. Even though silicon's silver repository is actually used for compilation of ViperServer, we assume that both reference the same silver commit.
Compile by typing: sbt compile
Other supported SBT commands are: sbt stage (produces fine-grained jar files), sbt assembly (produces a single fat jar file).

Set the environment variable Z3_EXE to an executable of a recent version of Z3.
Set the environment variable BOOGIE_EXE to an executable of a recent version of Boogie
Run the following command: sbt test.