Semantics and Verification of Object-Oriented Languages

Icon

NII Shonan Meeting Seminar 063

Alex Summers: The Viper Project: Verification Infrastructure for Permission-based Reasoning

Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade. However, verification approaches geared around complex program logics (such as separation logic) have typically been implemented in specialised tools, since the reasoning is hard to map down to first-order automated reasoning. In practice, this means that a rich variety of modern techniques have no corresponding tool support.

In this talk, I will present the new Silver intermediate verification language, which has been designed to facilitate the lightweight implementation of a variety of modern methodologies for program verification. In contrast to lower-level verification languages, Silver provides native support for heap reasoning; modes of reasoning such as concurrent separation logic, dynamic frames and rely-guarantee/invariants can be simply encoded.

Silver has been developed as part of the Viper project, which provides two automated back-end verifiers for Silver programs. Since releasing our software in September last year, it has been used for (internal and external) projects to build tools for Java verification, non-blocking concurrency reasoning, flow-sensitive typing and reasoning about GPU and Linux kernel code.

Slides

Category: Talks

Tagged:

Comments are closed.