Jaehwang Jung (정재황)

I graduated with a PhD in Feb. 2025 and joined Rebellions Inc.

While at KAIST, I worked on design and verification of concurrent algorithms under supervision of Prof. Jeehoon Kang. Specifically, I focused on memory management algorithms for non-blocking concurrency and separation logics for weak memory models.

Contact

• Email: jaehwang.jung@kaist.ac.kr
• GitHub: tomtomjhj
• Bibliography: ORCID, DBLP, Google Scholar
• Place: Rm. 4441, Bldg. E3-1, KAIST (+82-42-350-7878)

Education

• (2025) Ph.D. in Computer Science. KAIST (supervisor: Prof. Jeehoon Kang).

• (2020) B.S. in Computer Science. KAIST.

Publications

• (PLDI 2025) Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic.
  Jaehwang Jung, Sunho Park, Janggun Lee, Jeho Yeon, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation (Distinguished Paper Award).
  [paper: doi, local] ​ ​ ​
  

• (PLDI 2025) Verifying Lock-Free Traversals in Relaxed Memory Separation Logic.
  Sunho Park, Jaehwang Jung, Janggun Lee, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ ​ ​
  

• (Ph.D. Dissertation 2025) Design and Verification of Concurrent Memory Reclamation Algorithms.
  Jaehwang Jung .
  School of Computing, KAIST (Outstanding PhD Thesis Award).
  [paper: local] ​ ​ ​
  

• (SPAA 2024) Expediting Hazard Pointers with Bounded RCU Critical Sections.
  Jeonghyeon Kim, Jaehwang Jung, Jeehoon Kang .
  ACM Symposium on Parallelism in Algorithms and Architectures (Best Paper Award).
  [paper: doi, local] ​ [artifact: benchmark] ​ ​
  

• (PLDI 2024) Concurrent Immediate Reference Counting.
  Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ [artifact: benchmark] ​ ​
  

• (PLDI 2024) A Proof Recipe for Linearizability in Relaxed Memory Separation Logic.
  Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ [artifact: proofs] ​ ​
  

• (OOPSLA 2023) Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic.
  Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang .
  Object-oriented Programming, Systems, Languages, and Applications.
  [paper: doi, local] ​ [artifact: proofs] ​ ​
  

• (SPAA 2023) Applying Hazard Pointers to More Concurrent Data Structures.
  Jaehwang Jung, Janggun Lee, Jeonghyeon Kim, Jeehoon Kang .
  ACM Symposium on Parallelism in Algorithms and Architectures.
  [paper: doi, local] ​ [artifact: development, benchmark] ​ ​
  

• (PLDI 2022) Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic.
  Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ ​ ​
  

• (PLDI 2020) A Marriage of Pointer- and Epoch-Based Reclamation.
  Jeehoon Kang, Jaehwang Jung .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ [artifact: benchmark] ​ ​
  

Experiences

• Intern, Runtime Verification Inc., May, 2018 - August, 2018, January, 2019 - February 2019.

  (topic: verification of ethereum smart contracts)