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.

The Purpose of ViperServer

1. 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/
2. 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
3. Avoid 1-3 second delays caused by JVM startup time. ViperServer offers a robust alternative to, e.g., Nailgun.
4. Develop Viper encodings more efficiently with caching.
5. 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/

Installation Instructions

• 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).

Running Tests

• Set the environment variable Z3_EXE to an executable of a recent version of Z3.

• Run the following command: sbt test.

Who do I talk to?

• This repository is maintained by Linard Arquint.