Jeonghyeon Kim

I am a Ph.D. student at KAIST, currently advised by Prof. Youngjin Kwon in the School of Computing.

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

Research Interests

My research focuses on concurrent memory reclamation and formal verification of distributed systems.

Concurrent Memory Reclamation

I design efficient memory reclamation methods for concurrent systems. My initial work contributed to HP++, an extension of Hazard Pointers (SPAA 2023).

I developed a Safe Memory Reclamation (SMR) scheme combining Hazard Pointers with bounded RCU critical sections, improving the trade-off between memory footprint and performance (Best Paper Award, SPAA 2024).

Ongoing:

Developing a lock-free, precise garbage collection library.

Formal Verification of Distributed Systems

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

Ongoing:

Contributing to a top-down verification framework for weakly consistent systems (with Northeastern and Yonsei University). I focus on liveness properties such as convergence and availability, including the first known formalization of availability in this context.

Selected Publications

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.

PLOS 2025 DOI

Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals

Janggun Lee, Jeonghyeon Kim, Jeehoon Kang.

PLDI 2025 DOI Paper Proof Benchmark

Expediting Hazard Pointers with Bounded RCU Critical Sections

Jeonghyeon Kim, Jaehwang Jung, Jeehoon Kang.

SPAA 2024 🏆 Best Paper Award DOI Paper Slides Benchmark

Concurrent Immediate Reference Counting

Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang.

PLDI 2024 DOI Paper Benchmark

Applying Hazard Pointers to More Concurrent Data Structures

Jaehwang Jung, Janggun Lee, Jeonghyeon Kim, Jeehoon Kang.

SPAA 2023 DOI Paper Benchmark

News & Awards

June 2024

Best Paper Award

"Expediting Hazard Pointers with Bounded RCU Critical Sections" at SPAA 2024.

December 2022

2nd Place

Goorm Algorithm Monday Challenge.

August 2022

Salutatorian (Second Highest Distinction)

University of Seoul, B.S. in Computer Science.

July 2022

Encouragement Award

Hyundai Mobis Algorithm Competition.