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

New for: D1, D2, D3, D4, D5
<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:RustBelt: Logical Foundations for the Future of Safe Systems Programming
Speaker:Derek Dreyer
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:Joint Lecture Series
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 4 May 2016
Duration:60 Minutes
Building:E1 5
Rust is a new language developed at Mozilla Research that marries

together the low-level flexibility of modern C++ with a strong
"ownership-based" type system guaranteeing type safety, memory safety,
and data race freedom. As such, Rust has the potential to
revolutionize systems programming, making it possible to build
software systems that are safe by construction, without having to give
up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally
investigated, and it is not at all clear that they hold. To rule out
data races and other common programming errors, Rust's core type
system prohibits the aliasing of mutable state.  This is too
restrictive, however, for a number of essential data structures, and
thus Rust's standard libraries make widespread internal use of
"unsafe" features of the language.  The Rust developers claim that
such "unsafe" code has been properly encapsulated, so that Rust's
language-level safety guarantees are preserved, but this claim is
called into question by various safety bugs uncovered in Rust in the
past year.

In the RustBelt project, funded by an ERC Consolidator Grant, we aim
to develop the first formal tools for verifying the safety of Rust.
To tackle this challenge, we will build on recent breakthrough
developments in the area of Concurrent Separation Logic, in particular
our work on the Iris and GPS program logics.  In the talk, I will
explain what Concurrent Separation Logic is, why it is relevant to the
Rust verification effort, what problems remain in developing a program
logic suitable for Rust, and how Iris and GPS make progress toward
that goal.

Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Brigitta Hansen, 06/16/2016 11:23 AM
  • Jennifer Müller, 03/31/2016 11:22 AM -- Created document.