/viper-ide

This is the main repository for the Viper IDE extension for VS Code.

Primary LanguageTypeScriptMozilla Public License 2.0MPL-2.0

Test Status License: MPL 2.0

This VS Code extension provides interactive IDE features for Viper — the Verification Infrastructure for Permission-based Reasoning.

Dependencies

The extension automatically downloads and manages Viper (via publicly available links, as listed here: http://viper.ethz.ch/downloads/).

Viper IDE uses an open-source 64-bit Java server, so you need Java (version 11 or newer) installed to be able to run it.

Please always refer to the official installation instructions for more details (in particular, about different operating system support).

Using Viper

If you would like to learn more about Viper, please start with our extensive tutorial.

Debugging verification failures

Lizard is a (visual) verification debugger prototype for Viper IDE. It aims at simplifying the understanding of verification failures by converting SMT models to counterexample diagrams that are shown next to the code.