Viper

Main content

Viper (Verification Infrastructure for Permission-based Reasoning) is a 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, Silver, 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 Silver.

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 Silver, 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 Silver. Our toolset is also currently used as a back-end for the VerCors project at the University of Twente.

You can try out the Viper tools directly, at Viper Online. There is also a plugin for VSCode available for download.

Tool Details

Accordion. Press Tab to navigate to entries, then Enter to open or collapse content.

 

Silver

The Silver intermediate verification language 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. Silver 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.

Carbon

Carbon is one of the two provided verifiers for Silver programs, based on a translation from Silver to the Boogie verification language. The source code for Carbon is available in our Bitbucket repository.

Silicon

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

Chalice2Silver

Chalice2Silver is an example front-end verifier for the Chalice research language, implemented via a translation to Silver. 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.

Key Publications

  • 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. To appear. [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

The following students have contributed to the current Viper tools via previous projects: Christian Klauser, Stefan Heule, Bernard Brodowsky, Severin Heiniger, Simon Fritsche. Viper has also greatly benefited from the contributions of our former team members Pietro Ferrara, Uri Juhasz, Ioannis Kassios and Milos Novacek.

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

 
 
Page URL: http://www.pm.inf.ethz.ch/research/viper.html
27.04.2017
© 2017 Eidgenössische Technische Hochschule Zürich