Sotabase

Career

· Assistant Professor, ETH Zurich2022–
· Post-doctoral researcher, MIT2021–2022
· Post-doctoral researcher, MPI-SWS2020–2021
· Internship and research assistantship, Mozilla Research2017–
· Research assistant, Saarland University2014–
· Master in Computer Science, MPI-SWS and Saarland University2013–2019
· PhD in Computer Science, Saarland University2013–2020
· Bachelor in Computer Science, Saarland University2010–2013

Publications (24)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Journal of functional programming · 2018
421
cited
RustBelt: securing the foundations of the rust programming language
Proc. ACM Program. Lang. · 2017
418
cited
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
ACM-SIGACT Symposium on Principles of Programming Languages · 2015
359
cited
Higher-order ghost state
ACM SIGPLAN International Conference on Functional Programming · 2016
149
cited
The Essence of Higher-Order Concurrent Separation Logic
European Symposium on Programming · 2017
143
cited
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
Proc. ACM Program. Lang. · 2018
89
cited
Stacked borrows: an aliasing model for Rust
Proc. ACM Program. Lang. · 2019
82
cited
The future is ours: prophecy variables in separation logic
Proc. ACM Program. Lang. · 2019
70
cited
Safe systems programming in Rust
Communications of the ACM · 2021
60
cited
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
European Symposium on Programming · 2017
49
cited
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
Proc. ACM Program. Lang. · 2024
37
cited
Simuliris: a separation logic framework for verifying concurrent program optimizations
Proc. ACM Program. Lang. · 2022
36
cited
Understanding and evolving the Rust programming language
2020
35
cited
GoJournal: a verified, concurrent, crash-safe journaling system
USENIX Symposium on Operating Systems Design and Implementation · 2021
30
cited
Reconciling high-level optimizations and low-level code in LLVM
Proc. ACM Program. Lang. · 2018
30
cited
GhostCell: separating permissions from data in Rust
Proc. ACM Program. Lang. · 2021
25
cited
Later credits: resourceful reasoning for the later modality
Proc. ACM Program. Lang. · 2022
24
cited
Grove: a Separation-Logic Library for Verifying Distributed Systems
Symposium on Operating Systems Principles · 2023
23
cited
Verifying vMVCC, a high-performance transaction library using multi-version concurrency control
USENIX Symposium on Operating Systems Design and Implementation · 2023
15
cited
Resourceful Reasoning for the Later Modality
2022
1
cited
Sotabase
Ralf Jung | Researcher Profile | Sotabase | Sotabase