May 18, 2018Presentation: Viper: A Verification Infrastructure for Permission-based Reasoning
Room: Zi 2126Alex Summers

Modern verification techniques are becoming ever-more powerful and
sophisticated, and building tools that make these available to a wider
community is a challenging research area. Implementing a new program verifier
from scratch to validate each on-paper approach is time-consuming and
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 (e.g.  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; methodologies such as concurrent separation logic,
dynamic frames and two-state invariants can be simply encoded, enabling new
research prototypes to be developed efficiently. Viper has been used at ETH
Zurich and other universities for building verifiers for Java and Python,
applying techniques for non-blocking concurrency and information flow proofs,
and reasoning about GPU kernel code. I’ll give an introduction to the language
itself, and illustrate it with a recent application: deductive verification for
C11 weak memory primitives.