This is ViperServer, an HTTP server that manages verification requests to different tools from the Viper tool stack.
The main two tools 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/
- 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, please visit: http://viper.ethz.ch/downloads/
- Clone silver, silicon and carbon repositories in your computer, in separate directories.
- Clone viperserver (this repository) in your computer, in another directory.
- From within the directory where you installed viperserver, create a symbolic links to the directories where you installed silver, silicon and carbon.
- On Linux/Mac OS X:
ln -s <relative path to diretory where you installed silver> silver
ln -s <relative path to diretory where you installed silicon> silicon
ln -s <relative path to diretory where you installed carbon> carbon
- On Windows:
mklink /D silver <relative path to diretory where you installed silver>
mklink /D silicon <relative path to diretory where you installed silicon>
mklink /D carbon <relative path to diretory where you installed carbon>
-
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_EXEto an executable of a recent version of Z3. -
Run the following command:
sbt test.
- This repository is maintained by Arshavir Ter-Gabrielyan.