Janggun Lee (이장건)

I am a Ph.D Student at KAIST School of Computing at Concurrency and Parallelism Laboratory.

My interest lies in formal verfication low-level concurrent data structures and systems. I am especially interested in modular and automatic verification of them using separation logic such as Iris.

Contact

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

Education

• (2024 - Current) Ph.D. in Computer Science. KAIST.

• (2024) M.S. in Computer Science. KAIST.

• (2022) B.S. in Mathematical Sciences & Computer Science. KAIST.

Publications

• (PLDI 2025) Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals.
  Janggun Lee, Jeonghyeon Kim, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ [artifact: proofs, benchmark] ​ ​
  

• (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] ​ ​ ​
  

• (OOPSLA 2025) Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness.
  Dongjae Lee, Janggun Lee, Taeyoung Yoon, Minki Cho, Jeehoon Kang, Chung-Kil Hur .
  Object-oriented Programming, Systems, Languages, and Applications.
  [paper: doi, local] ​ ​ ​
  

• (OOPSLA 2024) Quantum Probabilistic Model Checking for Time-bounded Properties.
  Seungmin Jeon, Kyeongmin Cho, Chan Gu Kang, Janggun Lee, Hakjoo Oh, Jeehoon Kang .
  Object-oriented Programming, Systems, Languages, and Applications.
  [paper: doi, local] ​ ​ ​
  

• (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] ​ ​