Ralf Jung
where else to find them
website:https://www.ralfj.de
github:RalfJung
what they talk about
all 7 in the filters
where they keep going back
- POPL3 editions2022–2026
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
all 9 in the filters
on a stage with
all 31 in the filters
who talks about the same things
- Derek Dreyer35 talks
- Michael Sammler16 talks
- Lennard Gäher7 talks
- Oli Scherer4 talks
- Alexander J. Summers13 talks
- Ranjit Jhala19 talks
| title | conference | date |
|---|---|---|
| Miri: Practical Undefined Behavior Detection for Rust | POPL 2026 | 2026-01-11 |
Miri is an interpreter of Rust’s abstract machine that tracks per-byte initialization and pointer provenance, enforces Rust type representations, detects data… | ||
| What's the deal with unsafe Rust? | Scala Days 2025 | 2025-08-19 |
Explains why unsafe Rust exists, shows Mini Rust spec as an executable operational semantics and the MIRI interpreter as a tester, and demonstrates a real UB… | ||
| Functional Programming And the Real World | Scala Days 2025 | 2025-08-19 |
Panelists argue concrete claims: Rust is argued to be effectively functional in safe code and NAS translates Rust to Lean for verification; Zig and Rust trade… | ||
| Panel: Mechanized Specifications for Real-World Programming Languages | RPLS 2025 | 2025-06-17 |
Panelists contrast concrete outcomes: an K framework built for engineering-first, executable semantics; a call for a usable symbolic executor for P4 that can… | ||
| MiniRust: A Core Language for Specifying Rust | RPLS 2025 | 2025-06-17 |
Two demos show concrete, reproducible failures: reading an uninitialized i8 decodes to an error and the interpreter flags undefined behavior at decode time… | ||
| Tree Borrows | PLDI 2025 | 2025-06-16 |
Replaces Stacked Borrows’ stack with a per-allocation tree and formalizes aliasing rules so compilers can assume those violations are UB while accepting many… | ||
| MiniRust: A core language for specifying Rust | RustWeek 2025 | 2025-05-13 |
MiniRust is a precise, operational core language plus an executable interpreter (Specker) that lowers Rust and answers whether a program has UB by running the… | ||
| Program logics à la carte | POPL 2025 | 2025-01-19 |
Combines reusable program-logic fragments for language effects (shared state, concurrency, nondeterminism) so logics can be composed rather than rebuilt. Uses… | ||
| Rustlantis: Randomized Differential Testing of the Rust Compiler | OOPSLA 2024 | 2024-10-20 |
Rustlantis is a randomized differential fuzzer that generates MIR directly and targets rustc backends (LLVM and Cranelift) plus Miri to detect UB. It… | ||
| RefinedRust: A Type System for High-Assurance Verification of Rust Programs | PLDI 2024 | 2024-06-24 |
RefinedRust presents a refinement type system that verifies both unsafe Rust and safe Rust by translating MIR into a Coq-embedded Rust model and checking… | ||
| Verifying vMVCC, a high-performance transaction library using multi-version concurrency.. | OSDI 2023 | 2023-07-10 |
vMVCC claims to be the first MVCC transaction library with a machine-checked proof and ships as about 800 lines of Go (open source). It implements in-memory… | ||
| Later Credits: Resourceful Reasoning for the Later Modality | ICFP 2022 | 2022-09-11 |
Introduces later credits as an ownable resource in Iris that splits stepping into a credit-generation rule and a credit-spending rule, letting proofs prepay… | ||
| Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz | POPL 2022 | 2022-01-16 |
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler… | ||
| GoJournal: a verified, concurrent, crash-safe journaling system | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
GoJournal implements a verified, concurrent, crash-safe journaling API in Go and proves it in Coq with Perennial 2.0, using the Goose translator to model Go… | ||
| nothing matches | ||