/viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.

Primary LanguageScalaOtherNOASSERTION

Test Status License: MPL 2.0

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?