Jaehwang Jung (정재황)

I am expected to graduate with a PhD in Feb. 2025. I am looking for a position in a Korean organization (industry or academia) that can host a 전문연구요원.

I am a PhD candidate at Concurrency and Parallelism Laboratory, KAIST School of Computing. I have been working on design and verification of algorithms for concurrency, especially 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 (to appear).
  ​ ​ ​
  

• (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 (to appear).
  ​ ​ ​
  

• (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: Coq 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: Coq 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)