MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Prusti – Deductive Verification for Rust

Alex Summers
ETH Zurich
SWS Colloquium

Alex Summers works broadly on program verification techniques and tools, specialising in imperative concurrent languages,
and modular deductive verification. Alex obtained his PhD from Imperial College London, worked as a postdoc at Imperial College
London and ETH Zurich, and then as a Senior Researcher (Oberassistent) at ETH Zurich. He currently coordinates the Viper and
Prusti research projects. In March 2020 he will start a new position as Associate Professor at the University of British Columbia.
INET, SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Tuesday, 3 December 2019
10:30
90 Minutes
G26
111
Kaiserslautern

Abstract

Producing reliable systems software is a major challenge, plagued by the ubiquitous problems of shared mutable state, pointer
aliasing, dynamic memory management, and subtle concurrency issues such as race conditions; even expert programmers struggle
to tame the wide variety of reasons why their programs may not behave as they intended. Formal verification offers potential solutions
to many of these problems, but typically at a very high price: the mathematical techniques employed are highly-complex, and difficult
for even expert researchers to understand and apply.

The relatively-new Rust programming language is designed to help with the former problem: a powerful ownership type system
requires programmers to specify and restrict their discipline for referencing heap locations, providing in return the strong guarantee
(almost – the talk, and Rustbelt!) that code type-checked by this system will be free from dangling pointers, unexpected aliasing,
race conditions and the like. While this rules out a number of common errors, the question of whether a program behaves as
intended remains.

In this talk, I’ll give an overview of the Prusti project, which leverages Rust’s type system and compiler analyses for formal verification.
By combining the rich information available about a type-checked Rust program with separate user-specification of intended behaviour,
Prusti enables a user to verify functional correctness of their code without interacting with a complex program logic; in particular,
specifications and all interactions with our implemented tool are at the level of abstraction of Rust expressions.

Contact

Annika Meiser
93039105
--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
029
SWS Space 2 (6312)
passcode not visible
logged in users only

Annika Meiser, 11/28/2019 09:23 -- Created document.