Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. - Ralf Jung 002; David Swasey; Filip Sieczkowski; Kasper Svendsen; Aaron Turon; Lars Birkedal; Derek Dreyer (POPL, 2015)

Higher-order ghost state. - Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (ICFP, 2016)

The Essence of Higher-Order Concurrent Separation Logic. - Robbert Krebbers; Ralf Jung 002; Ales Bizjak; Jacques-Henri Jourdan; Derek Dreyer; Lars Birkedal (ESOP, 2017)

A Higher-Order Logic for Concurrent Termination-Preserving Refinement. - Joseph Tassarotti; Ralf Jung 002; Robert Harper 001 (ESOP, 2017)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic. - Ralf Jung 002; Robbert Krebbers; Jacques-Henri Jourdan; Ales Bizjak; Lars Birkedal; Derek Dreyer (J. Funct. Program., 2018)

RustBelt: securing the foundations of the rust programming language. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 2018)

Reconciling high-level optimizations and low-level code in LLVM. - Juneyoung Lee; Chung-Kil Hur; Ralf Jung 002; Zhengyang Liu 003; John Regehr; Nuno P. Lopes (Proc. ACM Program. Lang., 2018)

Stacked borrows: an aliasing model for Rust. - Ralf Jung 002; Hoang-Hai Dang; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2020)

The future is ours: prophecy variables in separation logic. - Ralf Jung 002; Rodolphe Lepigre; Gaurav Parthasarathy; Marianna Rapoport; Amin Timany; Derek Dreyer; Bart Jacobs 002 (Proc. ACM Program. Lang., 2020)

Understanding and evolving the Rust programming language. - Ralf Jung 002 (2020)

Verständnis und Weiterentwicklung der Programmiersprache Rust. - Ralf Jung 002 (Ausgezeichnete Informatikdissertationen, 2020)

GoJournal: a verified, concurrent, crash-safe journaling system. - Tej Chajed; Joseph Tassarotti; Mark Theng; Ralf Jung 002; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2021)

Safe systems programming in Rust. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Commun. ACM, 2021)

GhostCell: separating permissions from data in Rust. - Joshua Yanovski; Hoang-Hai Dang; Ralf Jung 002; Derek Dreyer (Proc. ACM Program. Lang., 2021)

Simuliris: a separation logic framework for verifying concurrent program optimizations. - Lennard Gäher; Michael Sammler; Simon Spies; Ralf Jung 002; Hoang-Hai Dang; Robbert Krebbers; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Later credits: resourceful reasoning for the later modality. - Simon Spies; Lennard Gäher; Joseph Tassarotti; Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. - Yun-Sheng Chang; Ralf Jung 002; Upamanyu Sharma; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2023)

Grove: a Separation-Logic Library for Verifying Distributed Systems. - Upamanyu Sharma; Ralf Jung 002; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (SOSP, 2023)

Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version). - Upamanyu Sharma; Ralf Jung 002; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (CoRR, 2023)

RefinedRust: A Type System for High-Assurance Verification of Rust Programs. - Lennard Gäher; Michael Sammler; Ralf Jung 002; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2024)

Rustlantis: Randomized Differential Testing of the Rust Compiler. - Qian Wang; Ralf Jung 002 (Proc. ACM Program. Lang., 2024)

Reproduction Image for Article 'Rustlantis: Randomized Differential Testing of the Rust Compiler'. - Andy Wang; Ralf Jung 002 (Zenodo, 2024)

Tree Borrows. - Neven Villani; Johannes Hostert; Derek Dreyer; Ralf Jung 002 (Proc. ACM Program. Lang., 2025)

Program Logics à la Carte. - Max Vistrup; Michael Sammler; Ralf Jung 002 (Proc. ACM Program. Lang., 2025)