[Pl-seminar] PRL Seminar TOMORROW 8/11 at 11:45am: Alex Summers, Viper: Verification Infrastructure for Permission-based Reasoning

[William J. Bowman]

NUPRL Seminar presents

Alex Summers
ETH Zürich (https://www.ethz.ch/en.html)

Host: Amal Ahmed

11:45am--1:25pm
Tuesday, Aug. 11th 2015
Room 166 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Viper: Verification Infrastructure for Permission-based Reasoning

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

Bio:
Alex Summers obtained his PhD from Imperial College London in 2009, in the area of type systems and classical logics. Since then 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.

-- 
William J. Bowman
Northeastern University
College of Computer and Information Science
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: Digital signature
URL: <http://lists.ccs.neu.edu/pipermail/pl-seminar/attachments/20150810/06f156cf/attachment.pgp>