Presentation: Viper: A Verification Infrastructure for Permission-based Reasoning

When: May 18, 2018, 11:00-12:00

Where: Zi 2126

Who: Alex 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
verification approaches geared around advanced program logics (e.g.  separation
corresponding tool support available.

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