ERC Project "RustBelt"

Update

The ERC-funded RustBelt project has now formally ended (as of April 2021), but the project continues in spirit, and we continue to seek exceptional candidates for PhD and postdoc positions at MPI-SWS. We look forward to continued exploration of Rust, Iris, separation logic, relaxed memory models, and more. See below for information on how to apply.

Original announcement

We are very pleased to announce the awarding of a 2015 ERC Consolidator Grant for the project "RustBelt: Logical Foundations for the Future of Safe Systems Programming". The project concerns the development of rigorous formal foundations for the Rust programming language (see project summary below).

The project is 5 years long and will include funding for several postdoc and PhD student positions supervised by Derek Dreyer at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany.

Open positions

Postdoctoral positions

For the postdoc positions, we are seeking exceptional candidates with a strong, internationally competitive track record of research in programming languages and/or verification. The primary criterion is quality, but we are particularly interested in candidates who have specialized expertise in one or more of the following areas:

  • Rust
  • substructural/ownership type systems
  • verification of concurrent programs
  • weak/relaxed memory models
  • interactive theorem proving in Coq
  • compiler verification
Experience programming in Rust is a welcome bonus, but not required.

PhD student positions

For the PhD student positions, we are seeking exceptional candidates who have at least some background in programming language theory and/or formal methods, and who are eager to work on deep foundational problems with the potential for direct impact on a real, actively developed language. A bachelor's or master's degree is required. Experience with Rust and/or Coq is a plus. The thesis research will be conducted under Dr. Dreyer's supervision at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany. The working language at MPI-SWS is English. (See here for more details about the graduate program at MPI-SWS).

How to apply

If you are interested in a postdoc or PhD position working on RustBelt, please send email directly to dreyer@mpi-sws.org, and also submit an application through the MPI-SWS application site. Please note in your application that you are interested in the RustBelt project. Starting dates are negotiable.

The RustBelt team

The Foundations of Programming group, led by Derek Dreyer at MPI-SWS, has a strong track record both in terms of publications and people. Current and former postdocs in the group have included Andreas Rossberg (co-designer of WebAssembly), Chung-Kil Hur, Neel Krishnaswami, Aaron Turon (former manager of the Rust project at Mozilla), Jacques-Henri Jourdan, Ori Lahav, Pierre-Marie Pédrot, Azalea Raad, and Rodolphe Lepigre. Current and former PhD students in the group have included Georg Neis, Beta Ziliani, Scott Kilpatrick, David Swasey, Ralf Jung, Jan-Oliver Kaiser, Hoang-Hai Dang, Marko Doko, Joshua Yanovski, Michael Sammler, and Simon Spies. The RustBelt project benefits from longstanding active collaborations with Deepak Garg (MPI-SWS), Viktor Vafeiadis (MPI-SWS), Lars Birkedal (Aarhus University), Chung-Kil Hur (Seoul National University), Jeehoon Kang (KAIST), Robbert Krebbers (TU Delft), and Joe Tassarotti (Boston College), as well as the many contributors to the Iris project.

Current Team Members @ MPI-SWS

Former Team Members @ MPI-SWS

We are collaborating actively with a number of researchers around the world on work that is directly relevant to the RustBelt project. We have generous funds available for members of the RustBelt team to travel and visit with our collaborators.

Project Collaborators

Summary of the RustBelt project proposal

A longstanding question in the design of programming languages is how to balance safety and control. C-like languages give programmers low-level control over resource management at the expense of safety, whereas Java-like languages give programmers safe high-level abstractions at the expense of control.

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, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art.

In this project, we aim to equip Rust programmers with the first formal tools for verifying safe encapsulation of "unsafe" code. Any realistic languages targeting this domain in the future will encounter the same problem, so we expect our results to have lasting impact. To achieve this goal, we will build on recent breakthrough developments by the PI and collaborators in concurrent program logics and semantic models of type systems.

RustBelt Publications

  1. GhostCell: Separating Permissions from Data in Rust.
    Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer.
    In ICFP 2021.
    (website with Rust and Coq development)

  2. GoJournal: A Verified, Concurrent, Crash-Safe Journaling System.
    Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich.
    In OSDI 2021.
    (source code, Coq development)

  3. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types.
    Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg.
    In PLDI 2021.
    (paper website, Coq development)
    Recipient of PLDI 2021 Distinguished Paper Award.
    Recipient of PLDI 2021 Distinguished Artifact Award.

  4. Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic.
    Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal.
    In PLDI 2021.
    (paper website, Coq development)

  5. Safe Systems Programming in Rust.
    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.
    In Communications of the ACM (CACM), 64(4): 144–152, April 2021.
    (paper in HTML, accompanying video)

  6. Transfinite Step-Indexing for Termination.
    Simon Spies, Neel Krishnaswami, Derek Dreyer.
    In POPL 2021.
    (technical appendix)

  7. Understanding and Evolving the Rust Programming Language.
    Ralf Jung.
    PhD dissertation, Saarland University, August 2020.
    Recipient of the 2020 ACM Doctoral Dissertation Award Honorable Mention
    Recipient of the 2021 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award
    Recipient of the 2021 ETAPS Doctoral Dissertation Award
    Recipient of the 2021 Otto Hahn Medal

  8. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic.
    Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn, Jules Villard.
    In CAV 2020.
    (paper website)

  9. Data Consistency in Transactional Storage Systems: A Centralised Semantics.
    Shale Xiong, Andrea Cerone, Azalea Raad, Philippa Gardner.
    In ECOOP 2020.

  10. RustBelt Meets Relaxed Memory.
    Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer.
    In POPL 2020.
    (paper website)

  11. Stacked Borrows: An Aliasing Model for Rust.
    Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer.
    In POPL 2020.
    (paper website)

  12. The Future is Ours: Prophecy Variables in Separation Logic.
    Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs.
    In POPL 2020.
    (paper website)

  13. The High-Level Benefits of Low-Level Sandboxing.
    Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak.
    In POPL 2020.
    (Coq development)

  14. Persistency Semantics of the Intel-x86 Architecture.
    Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeadis.
    In POPL 2020.

  15. Weak Persistency Semantics from the Ground Up.
    Azalea Raad, John Wickerson, Viktor Vafeadis.
    In OOPSLA 2019.
    (paper website)

  16. Effective Lock Handling in Stateless Model Checking.
    Michalis Kokologiannakis, Azalea Raad, Viktor Vafeadis.
    In OOPSLA 2019.
    (paper website)

  17. Model Checking for Weakly Consistent Libraries.
    Michalis Kokologiannakis, Azalea Raad, Viktor Vafeadis.
    In PLDI 2019.
    (paper website)

  18. On Library Correctness under Weak Memory Consistency.
    Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, Viktor Vafeiadis.
    In POPL 2019.
    (paper website)

  19. On the Semantics of Snapshot Isolation.
    Azalea Raad, Ori Lahav, Viktor Vafeiadis.
    In VMCAI 2019.
    (paper website)

  20. Iris from the Ground Up:
    A Modular Foundation for Higher-Order Concurrent Separation Logic.
    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak,
    Lars Birkedal, Derek Dreyer.
    In Journal of Functional Programming (JFP), Volume 28, e20, November 2018.
    (Iris project webpage)
    This is a significantly revised and expanded synthesis of our ICFP 2016 and ESOP 2017 papers.

  21. Persistence Semantics for Weak Memory.
    Azalea Raad, Viktor Vafeiadis.
    In OOPSLA 2018.
    (paper website)

  22. MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic.
    Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer.
    In ICFP 2018.
    (website with Coq development, Iris project page)

  23. Mtac2: Typed Tactics for Backward Reasoning in Coq.
    Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer.
    In ICFP 2018.
    (website with Coq development, Iris project page)

  24. Failure is Not an Option: An Exceptional Type Theory.
    Pierre-Marie Pédrot, Nicolas Tabareau.
    In ESOP 2018.

  25. On Parallel Snapshot Isolation and Release/Acquire Consistency.
    Azalea Raad, Ori Lahav, Viktor Vafeiadis.
    In ESOP 2018.
    (paper website)

  26. A Separation Logic for a Promising Semantics.
    Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis.
    In ESOP 2018.
    (technical appendix)

  27. RustBelt: Securing the Foundations of the Rust Programming Language.
    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.
    In POPL 2018.
    (appendix and Coq development, Iris project webpage)

  28. Effective Stateless Model Checking for C/C++ Concurrency.
    Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis.
    In POPL 2018.
    (paper website)

  29. Robust and Compositional Verification of Object Capability Patterns.
    David Swasey, Deepak Garg, Derek Dreyer.
    In OOPSLA 2017.
    (Coq development)
    Recipient of OOPSLA 2017 Distinguished Paper Award.

  30. Strong Logic for Weak Memory:
    Reasoning About Release-Acquire Consistency in Iris.
    Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis.
    In ECOOP 2017.
    (website with Coq development and appendix)
    Recipient of ECOOP 2017 Distinguished Paper Award.

  31. Promising Compilation to ARMv8 POP.
    Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
    In ECOOP 2017.
    (paper website)

  32. Repairing Sequential Consistency in C/C++11.
    Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
    In PLDI 2017.
    Recipient of PLDI 2017 Distinguished Paper Award.

  33. The Essence of Higher-Order Concurrent Separation Logic.
    Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan,
    Derek Dreyer, Lars Birkedal.
    In ESOP 2017.
    (Iris 3.0 documentation, Iris project webpage)

  34. A Higher-Order Logic for Concurrent Termination-Preserving Refinement.
    Joseph Tassarotti, Ralf Jung, Robert Harper.
    In ESOP 2017.
    (paper website, arXiv version)

  35. A Promising Semantics for Relaxed-Memory Concurrency.
    Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
    In POPL 2017.
    (paper website with Coq development)

  36. Explaining Relaxed Memory Models with Program Transformations.
    Ori Lahav, Viktor Vafeiadis.
    In FM 2016.
    (paper website with Coq development)

  37. Higher-Order Ghost State.
    Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer.
    In ICFP 2016.
    (appendix, Iris 2.0 documentation, Coq development, talk video)

Related/Older Publications

Related projects

  • Iris: Higher-Order Concurrent Separation Logic in Coq
  • GPS: Strong Logic for Weak Memory
  • ModuRes: Modular Reasoning about Concurrent Higher-Order Imperative Programs
  • Mtac: A Monadically Typed Tactic Programming Language for Coq
Derek Dreyer
Valid XHTML 1.0 Transitional

Imprint / Data Protection