Viper

Main content

NEW: for an introduction to Viper's features, try the Viper Tutorial here!

Viper (Verification Infrastructure for Permission-based Reasoning) is a language and suite of tools developed at ETH Zurich, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. It comprises a novel intermediate verification language, also named Viper, and automatic verifiers for the language, as well as example front-end tools. The Viper toolset can be used to implement verification techniques for front-end programming languages via translations into the Viper language.

The Viper verification infrastructure

The Viper toolchain is designed to make it easy to implement verification techniques for programs with persistent mutable state (including concurrent programs), providing native support for reasoning about the program state using method permissions or ownership, e.g. in the style of separation logic. New verification techniques can be implemented directly as translations to the Viper language, using either of the verifiers provided.

In addition to the main tools detailed below, we have a prototype front-end for a subset of Scala, and are developing static analysis technology for Viper. Our toolset is also currently used as a back-end for the VerCors project at the University of Twente.

The best way to try out Viper for yourself is via the plugin for VSCode available for download. It is also possible to run Viper in your browser: there is an interactive introductory Viper tutorial available, as well as additional examples to try out online.

Tool Details

 

Viper Intermediate Language (Viper)

The Viper intermediate verification language (short: Viper) provides simple imperative constructs, as well as specifications and custom statements for managing permission-based reasoning. The assertion logic supported is a variant of implicit dynamic frames, which can be used to encode a variety of reasoning paradigms, including separation logics. Viper provides support for mathematical types, user-defined predicates and pure functions, and a number of other unique features based on recent research. More details can be found in the publications below, and source code is available.

Verification Condition Generation

One of the two provided verifiers for Viper programs uses verification condition generation. It is implemented via a translation from Viper to the Boogie verification language. The source code for this verifier is available in our Bitbucket repository.

Symbolic Execution

The other verifier for the Viper intermediate verification language is based on sound symbolic execution. It uses the Z3 SMT solver to discharge logical queries. Source code for the symbolic-execution verifier, as well as a wiki for helping new users, is available in our Bitbucket repository.

Chalice

The original implementation of the Chalice research language was based on Boogie. We re-implemented Chalice as a translation to Viper as an example front-end verifier. This implementation exploits many of Viper’s supported features, and outperforms the original Chalice implementation. Source code and further information is available in our Bitbucket repository.

Python

As part of the verifiedSCION project, we developed a program verifier for a statically-typed subset of Python. Source code and further information is available on GitHub.

Key Publications

  • A. J. Summers and P. Müller: Automating Deductive Verification for Weak-Memory Programs
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018.  [PDF][BIB]
  • P. Müller and M. Schwerhoff and A. J. Summers: Viper: A Verification Infrastructure for Permission-Based Reasoning
    Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016. [PDF][BIB]
  • P. Müller and M. Schwerhoff and A. J. Summers: Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution 
    Computer Aided Verification (CAV), 2016. [PDF][BIB]
  • M. Schwerhoff and A. J. Summers: Lightweight Support for Magic Wands in an Automatic Verifier
    European Conference on Object-Oriented Programming (ECOOP), 2015.  [PDF] [BIB] [Tool]
  • S. Heule and I. T. Kassios and P. Müller and A. J. Summers: Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions
    European Conference on Object-Oriented Programming (ECOOP),     2013. [PDF] [BIB]
  • M. J. Parkinson and A. J. Summers: The Relationship Between Separation Logic and Implicit Dynamic Frames
    Logical Methods in Computer Science,     2012. [PDF] [BIB]

Acknowledgments

Viper has also greatly benefited from the contributions of our former team members Pietro Ferrara, Uri Juhasz, Ioannis Kassios and Milos Novacek. We are also grateful to numerous students who contributed to Viper through their thesis projects. 

The Viper project has been funded by ETH Zurich, the Swiss National Science Foundation, and the Hasler Foundation.