EDBT 2026 Demo / reviewers in the wild / expert
Jeho Yeon
dblp:412/7863
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2025
0009-0000-7000-6836ORCID · reported
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
1 paper |
Concurrent programming · 56% Program verification · 44% |
Topics — the 6 heaviest of 6, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Concurrent programming
memory reclamation |
0.9 | 1 | 2025 | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic · Proc. ACM Program. Lang. 2025 |
Concurrent programming › synchronization
read-copy-update |
0.9 | 1 | 2025 | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic · Proc. ACM Program. Lang. 2025 |
Program verification › program logic
separation logic |
0.9 | 1 | 2025 | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic · Proc. ACM Program. Lang. 2025 |
Program verification › concurrent program verification
verification under weak memory models |
0.9 | 1 | 2025 | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic · Proc. ACM Program. Lang. 2025 |
Concurrent programming
memory models |
0.3 | 1 | 2025 | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic · Proc. ACM Program. Lang. 2025 |
Concurrent programming
synchronization |
0.3 | 1 | 2025 | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic · Proc. ACM Program. Lang. 2025 |
Methods — techniques the papers use, named apart from their topics
rocq · 0.9iris · 0.9iRC11 · 0.9
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation LogicabstractRead-Copy-Update (RCU) is a critical synchronization mechanism for concurrent data structures, enabling efficient deferred memory reclamation. However, implementing and using RCU correctly is challenging due to its inherent concurrency complexities. While previous work verified RCU, they either relied on unrealistic assumptions of sequentially consistent (SC) memory model or lacked three key features of general-purpose RCU libraries: modular specification, switchable critical sections, and concurrent writer support. We present the first formal verification of a general-purpose RCU in realistic relaxed memory consistency (RMC), addressing the challenges posed by these features. To achieve modular specification that encompasses relaxed behaviors, we extend existing SC specifications to account for explicit synchronization. To support switchable critical sections, which require read-after-write (RAW) synchronization, we introduce a reasoning principle for RAW-synchronizing SC fences . Using this principle, we also present the first formal verification of Peterson's mutex in RMC. To support concurrent writers performing partially ordered writes, we avoid assuming a total order of links and instead formulate invariants based on per-node incoming link histories. Our proofs are mechanized in the iRC11 relaxed memory separation logic, built upon Iris, in Rocq. Jaehwang Jung, Sunho Park, Janggun Lee, Jeho Yeon, Jeehoon Kang |
Proc. ACM Program. Lang. | 4 |