Jeonghyeon Kim
Ph.D. Student · School of Computing, KAIST

Jeonghyeon Kim

I am a Ph.D. student at KAIST, advised by Prof. Youngjin Kwon. My research builds principled foundations for high-performance concurrent systems—designing safe memory reclamation schemes for lock-free data structures and developing formal verification methodologies for weakly consistent distributed systems.

I am interested in problems where careful theory translates into measurable systems improvements: bridging the gap between hand-tuned concurrent algorithms and the rigorous arguments that justify them.

Recent Our paper "Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages" has been accepted to PLDI 2026. Preprint.
Jeonghyeon Kim

Education

Feb 2026 – Present
Ph.D. in Computer Science
KAIST, School of Computing Advised by Prof. Youngjin Kwon
Mar 2024 – Feb 2026
M.S. in AI Semiconductor
KAIST Advised by Prof. Jongse Park and Prof. Jeehoon Kang
Mar 2019 – Aug 2022
B.S. in Computer Science
University of Seoul Salutatorian (Second Highest Distinction)

Research

Concurrent Memory Reclamation

I design efficient and provably safe memory reclamation methods for concurrent data structures. My initial work contributed to HP++, an extension of Hazard Pointers that broadens their applicability to optimistic traversals (SPAA 2023). Building on this, I developed a Safe Memory Reclamation scheme that combines Hazard Pointers with bounded RCU critical sections to achieve a markedly better trade-off between memory footprint and runtime performance (Best Paper Award, SPAA 2024).

Ongoing Designing a lock-free, precise garbage collection library for unmanaged languages.

Formal Verification of Distributed Systems

I develop methodologies for formally verifying weakly consistent distributed systems, with attention to both safety and liveness properties.

Ongoing Contributing to a top-down verification framework for weakly consistent systems (joint work with collaborators at Northeastern and Yonsei). My focus is on liveness—convergence and availability—including the first known formalization of availability in this setting.

Publications

First-Authored

  1. PLDI 2026
    Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages
    Jeonghyeon Kim, Jongse Park, Youngjin Kwon, Jeehoon Kang
    DOI Preprint
    BibTeX 
    @article{kim2026partial,
  author    = {Kim, Jeonghyeon and Park, Jongse and Kwon, Youngjin and Kang, Jeehoon},
  title     = {Revisiting Partial Tracing for Safe, Efficient, and Concurrent
               Garbage Collection in Unmanaged Languages},
  journal   = {Proc. ACM Program. Lang.},
  volume    = {10},
  number    = {PLDI},
  articleno = {232},
  year      = {2026},
  month     = jun,
  doi       = {10.1145/3808310},
  note      = {To appear}
}
  2. SPAA 2024
    Expediting Hazard Pointers with Bounded RCU Critical Sections Best Paper
    Jeonghyeon Kim, Jaehwang Jung, Jeehoon Kang
    DOI Paper Slides Benchmark

Co-Authored

  1. PLOS 2025
    Compositional Model-Driven Verification of Weakly Consistent Distributed Systems
    Bryant J. Curto, Jeonghyeon Kim, Alan Wang, Gijung Im, Jieung Kim, Jeehoon Kang, Ji-Yong Shin
    DOI
  2. PLDI 2025
    Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
    Janggun Lee, Jeonghyeon Kim, Jeehoon Kang
    DOI Paper Proof Benchmark
  3. PLDI 2024
    Concurrent Immediate Reference Counting
    Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang
    DOI Paper Benchmark
  4. SPAA 2023
    Applying Hazard Pointers to More Concurrent Data Structures
    Jaehwang Jung, Janggun Lee, Jeonghyeon Kim, Jeehoon Kang
    DOI Paper Benchmark

News & Awards