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