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.
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.
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 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.
- 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]
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.