Chuchu Fan is the recipient of the 2020 ACM Doctoral Dissertation Award for her dissertation, “Formal Methods for Safe Autonomy: Data-Driven Verification, Synthesis, and Applications.” Honorable Mentions go to Henry Corrigan-Gibbs of the Massachusetts Institute of Technology and Ralf Jung of the Max Planck Institute for Software Systems and MIT.
Ralf Jung’s dissertation, “Understanding and Evolving the Rust Programming Language,” established the first formal foundations for safe systems programming in the innovative programming language Rust. In development at Mozilla since 2010, and increasingly popular throughout the industry, Rust addresses a longstanding problem in language design: how to balance safety and control. Like C++, Rust gives programmers low-level control over system resources. Unlike C++, Rust also employs a strong “ownership-based” system to statically ensure safety, so that security vulnerabilities like memory access errors and data races cannot occur. Prior to Jung’s work, however, there had been no rigorous investigation of whether Rust’s safety claims actually hold, and due to the extensive use of “unsafe escape hatches” in Rust libraries, these claims were difficult to assess.
In his dissertation, Jung tackles this challenge by developing semantic foundations for Rust that account directly for the interplay between safe and unsafe code. Building upon these foundations, Jung provides a proof of safety for a significant subset of Rust. Moreover, the proof is formalized within the automated proof assistant Coq and therefore its correctness is guaranteed. In addition, Jung provides a platform for formally verifying powerful type-based optimizations, even in the presence of unsafe code.
Through Jung's leadership and active engagement with the Rust Unsafe Code Guidelines working group, his work has already had profound impact on the design of Rust and laid essential foundations for its future.
Jung is a post-doctoral researcher at the Max Planck Institute for Software Systems and a research affiliate of the Parallel and Distributed Operating Systems Group at the Massachusetts Institute of Technology. His research interests include programming languages, verification, semantics, and type systems. He conducted his doctoral research at the Max Planck Institute for Software Systems, and received his PhD, Master's, and Bachelor's degrees in Computer Science from Saarland University.
