[Colloquium] CS Distinguished Lecture today at 3:00 pm - Derek Dreyer (MPI-SWS)

[Sandra Wallace]

UNIVERSITY OF CHICAGO
DEPARTMENT OF COMPUTER SCIENCE
DISTINGUISHED LECTURE SERIES

https://cs.uchicago.edu/page/distinguished-lecture-series <https://cs.uchicago.edu/page/distinguished-lecture-series>


Derek Dreyer 
MPI-SWS
http://www.mpi-sws.org/~dreyer <http://www.mpi-sws.org/~dreyer>

Thursday, May 12, 2016, 3:00 pm 
Ryerson 251


Title:  RustBelt: Logical Foundations for the Future of Safe Systems Programming

Abstract:
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 actually 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 subtle safety bugs uncovered in Rust in the past year.

In the RustBelt project, we aim to develop the first formal foundations for the safety of Rust programs.  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.


Bio:
Derek Dreyer heads the Foundations of Programming Group at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany, where he has been a member of the faculty since 2008 and received tenure in 2013.  He was previously a research assistant professor at Toyota Technological Institute at Chicago, after receiving his PhD from CMU in 2005.  He is a member of the editorial board of the Journal of Functional Programming, and was elected to serve on the ACM SIGPLAN Executive Committee from 2012 to 2015. 

Dr. Dreyer's research focuses on building foundations for modular, scalable verification of programs in *realistic* programming languages -- languages that combine complex features (e.g. closures, abstract data types, ownership types, weak-memory concurrency) in poorly understood ways.  Toward this end, he has recently been awarded a 2-million-euro Consolidator Grant from the European Research Council for the project RustBelt, concerning the development of rigorous formal foundations for safe systems programming in the Rust language.

Host: John Reppy


*Reception to follow in Ry. 255 at 4:00 pm*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20160512/f91d38c6/attachment.htm