Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
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:
- 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.
- This repository is maintained by Linard Arquint.