abstract:
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 for implementing research from a wide variety of domains, and several mature tools used in industry have been built around this common tool stack.
Reasoning approaches which orient around sophisticated partitioning and organisation of the verification state (such as separation logics) have typically been implemented in specialised tools, since the reasoning is hard to map down to first-order automated reasoning. In practice (with notable exceptions), 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.
bio:
Alex Summers obtained his PhD from Imperial College London in 2009, in the area of type systems and classical logics. Since 2008, he has worked in a variety of areas concerning software correctness and verification, at Imperial College London and ETH Zurich. His research interests include developing specification techniques for different (usually concurrent) programming paradigms, and implementing these in automatic verification tools. He was recently awarded the 2015 AITO Dahl-Nygaard Junior Prize for his work on type systems and the verification of object-oriented programs.