Ralf Jung

27 papers A* 4A 3Journal 17Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
Miri: Practical Undefined Behavior Detection for Rust.
Proc. ACM Program. Lang.
Ralf Jung, Benjamin Kimock, Christian Poveda, Eduardo Sánchez Muñoz, Oli Scherer, Qian Wang
2025 J jnl
Program Logics à la Carte.
Proc. ACM Program. Lang.
Max Vistrup, Michael Sammler, Ralf Jung
2025 J jnl
Tree Borrows.
Proc. ACM Program. Lang.
Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung
2024 J jnl
RefinedRust: A Type System for High-Assurance Verification of Rust Programs.
Proc. ACM Program. Lang.
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
2024 J jnl
Rustlantis: Randomized Differential Testing of the Rust Compiler.
Proc. ACM Program. Lang.
Qian Wang, Ralf Jung
2024 — conf
Stochastic Optimization of Hybrid Product Programs with Prepaid Contracts.
OR
Alexander Baumeister, Holger Hermanns, Ralf Jung
2023 J jnl
Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version).
CoRR
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2023 A* conf
Grove: a Separation-Logic Library for Verifying Distributed Systems.
SOSP
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2023 A* conf
Verifying vMVCC, a high-performance transaction library using multi-version concurrency control.
OSDI
Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2022 J jnl
Later credits: resourceful reasoning for the later modality.
Proc. ACM Program. Lang.
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2022 J jnl
Simuliris: a separation logic framework for verifying concurrent program optimizations.
Proc. ACM Program. Lang.
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
2021 J jnl
GhostCell: separating permissions from data in Rust.
Proc. ACM Program. Lang.
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer
2021 A* conf
GoJournal: a verified, concurrent, crash-safe journaling system.
OSDI
Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
2021 J jnl
Safe systems programming in Rust.
Commun. ACM
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2020 J jnl
Stacked borrows: an aliasing model for Rust.
Proc. ACM Program. Lang.
Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer
2020 J jnl
The future is ours: prophecy variables in separation logic.
Proc. ACM Program. Lang.
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
2020 — —
Understanding and evolving the Rust programming language.
Ralf Jung
2020 — ch.
Verständnis und Weiterentwicklung der Programmiersprache Rust.
Ausgezeichnete Informatikdissertationen
Ralf Jung
2018 J jnl
Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
J. Funct. Program.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
2018 J jnl
MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Proc. ACM Program. Lang.
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
2018 J jnl
Reconciling high-level optimizations and low-level code in LLVM.
Proc. ACM Program. Lang.
Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes
2018 J jnl
RustBelt: securing the foundations of the rust programming language.
Proc. ACM Program. Lang.
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2017 A conf
A Higher-Order Logic for Concurrent Termination-Preserving Refinement.
ESOP
Joseph Tassarotti, Ralf Jung, Robert Harper
2017 J jnl
A Higher-Order Logic for Concurrent Termination-Preserving Refinement.
CoRR
Joseph Tassarotti, Ralf Jung, Robert Harper
2017 A conf
The Essence of Higher-Order Concurrent Separation Logic.
ESOP
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
2016 A conf
Higher-order ghost state.
ICFP
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2015 A* conf
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.
POPL
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer