Viper
Main content
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 toolchain is designed to make it easy to implement verification techniques for sequential and concurrent programs with mutable state. It provides native support for reasoning about the program state using 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. The Viper language is also useful to encode verification problems manually, for instance, while prototyping new verification techniques.
We have built several verifiers on top of Viper, including the Gobra verifier for Go, Nagini for Python and Prusti for Rust. We have also built several research prototypes, for instance, for Chalice and to reason about weak-memory programs. Viper is also used outside ETH Zurich; the VerCors project at the University of Twente uses Viper as back-end for their Java and OpenCL verifiers. Jenna Wise is using Viper for her work on gradual verification. Viper is used for teaching at Charles University Prague, ETH Zurich, NYU, and Rice University.
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
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.
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 GitHub repository.
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 GitHub repository.
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.