Jeonghyeon Kim
I am a Master’s degree candidate at the KAIST Graduate School of AI Semiconductor, currently advised by Prof. Jongse Park in the School of Computing. From March 2024 to July 2025, I was fortunate to be advised by Prof. Jeehoon Kang in the Concurrency and Parallelism Laboratory. I earned my Bachelor’s degree in Computer Science from the University of Seoul, graduating as the Salutatorian (Second Highest Distinction).
My research interests lie at the intersection of concurrent systems and formal methods. I focus on developing practical concurrent memory reclamation techniques and formally verifying the correctness of critical distributed systems. You can find more details about my projects below.

Research Interests
This section introduces my main research areas. I am focused on enhancing the performance of concurrent systems and ensuring the reliability of distributed systems through rigorous verification.
Concurrent Memory Reclamation
My work involves designing practical and efficient memory reclamation methods for highly concurrent systems. I started this journey by contributing to the HP++ project, an extension of Hazard Pointers.
Building on that, I developed a novel Safe Memory Reclamation (SMR) scheme that combines classical Hazard Pointers with bounded RCU critical sections. This work enhances the balance between memory footprint and efficiency and was recognized with a Best Paper Award at SPAA 2024.
Ongoing Project:
I am currently developing a lock-free, precise garbage collection library with a focus on safety, efficiency, and seamless system integration.
Formal Verification of Distributed Systems
I focus on creating practical methodologies for formally verifying weakly consistent distributed systems to ensure both safety and liveness properties.
Ongoing Project:
I am a contributor to a novel top-down verification framework for weakly consistent systems, collaborating with researchers from Northeastern and Yonsei University. My role is centered on defining and proving key liveness properties, such as convergence and availability. This includes what we believe is the first formalization and verification of availability in this context.
Selected Publications
Here are some of my key publications. Each represents a significant step in my research journey, exploring various facets of concurrency and system verification.
Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
Janggun Lee, Jeonghyeon Kim, Jeehoon Kang.
PLDI 2025
Expediting Hazard Pointers with Bounded RCU Critical Sections
Jeonghyeon Kim, Jaehwang Jung, Jeehoon Kang.
SPAA 2024
🏆 Best Paper AwardConcurrent Immediate Reference Counting
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang.
PLDI 2024
News & Awards
This timeline highlights key moments and recognitions throughout my academic and competitive programming journey.
June 2024
Best Paper Award
Our paper, "Expediting Hazard Pointers with Bounded RCU Critical Sections," received the Best Paper Award at SPAA 2024.
December 2022
2nd Place
Awarded 2nd Place in the Goorm Algorithm Monday Challenge.
August 2022
Salutatorian (Second Highest Distinction)
Graduated with the second-highest academic standing from the University of Seoul.
July 2022
The Encouragement Award
Received at the '22 Hyundai Mobis Algorithm Competition.