Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Prusti – Deductive Verification for Rust
Speaker:Alex Summers
coming from:ETH Zurich
Speakers Bio: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.

Event Type:SWS Colloquium
Visibility:INET, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Tuesday, 3 December 2019
Duration:90 Minutes
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.
Name(s):Annika Meiser
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:029
Meeting ID:SWS Space 2 (6312)
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Annika Meiser, 11/28/2019 09:23 AM -- Created document.