/viperserver

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

Primary LanguageScalaOtherNOASSERTION

Scala CI

README

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?