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)