viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link
verification viper

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:

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

Running Tests

Who do I talk to?