Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Implementing a new verifier from scratch to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become a popular means of simplifying this task. However, verification approaches geared around advanced program logics (such as separation logics) are a difficult match for these (typically first-order) platforms. In practice, this means that a rich variety of modern techniques have no corresponding tool support available.

In this talk, I will present the Viper Project, which provides a new intermediate verification language designed to facilitate the lightweight implementation of a variety of modern methodologies for program verification. In contrast to lower-level verification languages, Viper provides native support for heap reasoning; modes of reasoning such as concurrent separation logic, dynamic frames and two-state invariants can be simply encoded, enabling new research prototypes to be developed efficiently.

Viper provides two automated back-end verifiers for general Viper programs. Since releasing the software 2 years ago, it has been used for (internal and external) projects, including verifiers for Java and Python, techniques for non-blocking concurrency reasoning, implementing flow-sensitive type systems and reasoning about GPU kernel code.