Viper
Viper (Verification Infrastructure for Permission-based Reasoning) is a language and suite of tools, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. Viper is being developed at ETH Zurich in close collaboration with the team of Alex Summers at UBC.
Viper 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. For an introduction to Viper's features, try the Viper Tutorial! You can download Viper here.
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, to reason about weak-memory programs, and to verify smart contracts written in the Vyper language. Viper is also used in various research projects outside ETH Zurich, e.g., at Brown University, CMU, Columbia University, INRIA, University of Minnesota, NYU, University of Twente (in the external pageVerCors project), and University of British Columbia. Viper is used for teaching at Charles University Prague, DTU Copenhagen, ETH Zurich, NYU, Rice University, and UBC.
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 external pagesource 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 external pageBoogie verification language. The source code for this verifier is available in our external pageGitHub 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 external pageGitHub repository.
Project Team
Viper is being developed in close collaboration with the team of Alex Summers at UBC.
Project Members at UBC
external pageDavid Ewert
external pageZack Grannan
external pageAlex Summers
ToTo Tokaeo
Links
See additional Viper examples online
external pageGet support on Stack Overflow
Source code for the core projects is open-sourced and external pagevailable on GitHub
Watch a Viper external pagepresentation
Viper versions of the examples and exercises from Rustan Leino's book external pageProgram Proofs
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. 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 external pageSwiss National Science Foundation, and the external pageHasler Foundation.