Publications

Conference and journal papers

2025

• Tree Borrows
  Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung
  In PLDI 2025, Distinguished Paper Award
  [paper] [paper website]

• Program Logics à la Carte
  Max Vistrup, Michael Sammler, Ralf Jung
  In POPL 2025
  [paper] [paper website]

2024

• Rustlantis: Randomized Differential Testing of the Rust Compiler
  Qian Wang, Ralf Jung
  In OOPSLA 2024
  [paper] [paper website]

• RefinedRust: A Type System for High-Assurance Verification of Rust Programs
  Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
  In PLDI 2024
  [paper] [paper website]

2023

• Grove: a Separation-Logic Library for Verifying Distributed Systems
  Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
  In SOSP 2023
  [paper] [extended version]

• Verifying vMVCC, a high-performance transaction library using multi-version concurrency control
  Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
  In OSDI 2023
  [paper] [paper website]

2022

• Later Credits: Resourceful Reasoning for the Later Modality
  Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
  In ICFP 2022
  [paper] [paper website]

• Simuliris: A separation logic framework for verifying concurrent program optimizations
  Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
  In POPL 2022, Distinguished Paper Award
  [paper]

2021

• GhostCell: Separating Permissions from Data in Rust
  Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer
  In ICFP 2021
  [paper] [paper website]

• GoJournal: a verified, concurrent, crash-safe journaling system
  Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
  In OSDI 2021
  [paper]

• Safe Systems Programming in Rust: The Promise and the Challenge
  Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
  In Communications of the ACM (CACM)
  [article] [pdf] [video]

2020

• 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] [paper website]

• Stacked Borrows: An Aliasing Model for Rust
  Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer
  In POPL 2020
  [paper] [paper website]

2018

• 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
  [paper] [project website]

• Reconciling High-Level Optimizations and Low-Level Code in LLVM
  Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes
  In OOPSLA 2018
  [paper] [paper website]

• 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
  [paper] [paper website]

• RustBelt: Securing the Foundations of the Rust Programming Language
  Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
  In POPL 2018
  [paper] [paper website] [talk (YouTube)] [talk (slides)]

2017

• The Essence of Higher-Order Concurrent Separation Logic
  Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
  In ESOP 2017
  [paper] [project website]

• A Higher-Order Logic for Concurrent Termination-Preserving Refinement
  Joseph Tassarotti, Ralf Jung, Robert Harper
  In ESOP 2017
  [paper] [paper website]

2016

• Higher-Order Ghost State
  Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
  In ICFP 2016
  [paper] [project website] [talk (YouTube)] [talk (slides)]

2015

• Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
  Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
  In POPL 2015, Most Influential Paper Award
  [paper] [project website] [talk (slides)]

Theses

2020

• Understanding and Evolving the Rust Programming Language
  Ralf Jung
  PhD Thesis
  [website]

2019

• Higher-Order Ghost State
  Ralf Jung
  Master Thesis
  [based on this paper]

2013

• An Intermediate Language To Formally Justify Memory Access Reordering
  Ralf Jung
  Bachelor Thesis
  [thesis] [slides] [coq]