Ralf Jung

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 19

Top Topics

Distributed Systems

Orthogonal Basis

Higher Order Logic

Programming Language

Top Venues

Proc. ACM Program. Lang.

Publications

Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. OSDI (2023)
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Grove: a Separation-Logic Library for Verifying Distributed Systems. SOSP (2023)
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version). CoRR (2023)
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6 (POPL) (2022)
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer
GhostCell: separating permissions from data in Rust. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
Safe systems programming in Rust. Commun. ACM 64 (4) (2021)
Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
GoJournal: a verified, concurrent, crash-safe journaling system. OSDI (2021)
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4 (POPL) (2020)
Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer
Stacked borrows: an aliasing model for Rust. Proc. ACM Program. Lang. 4 (POPL) (2020)
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2 (POPL) (2018)
Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes
Reconciling high-level optimizations and low-level code in LLVM. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
The Essence of Higher-Order Concurrent Separation Logic. ESOP (2017)
Joseph Tassarotti, Ralf Jung, Robert Harper
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. ESOP (2017)
Joseph Tassarotti, Ralf Jung, Robert Harper
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. CoRR (2017)
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Higher-order ghost state. ICFP (2016)
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. POPL (2015)