Publications

Preprints / Under Submission

• Formal Verification of an Out-of-Order Multiprocessor against an In-Order Weak-Memory ISA
  Janggun Lee , Jeehoon Kang
  Under submission, 2026
  [PDF]

2025

• Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
  Janggun Lee , Jeonghyeon Kim , Jeehoon Kang
  PLDI, 2025
  [PDF] [DOI]
• Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
  Jaehwang Jung , Sunho Park , Janggun Lee , Jeho Yeon , Jeehoon Kang
  PLDI, 2025 · Distinguished Paper Award
  [PDF] [DOI]
• Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
  Sunho Park , Jaehwang Jung , Janggun Lee , Jeehoon Kang
  PLDI, 2025
  [PDF] [DOI]
• Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
  Dongjae Lee , Janggun Lee , Taeyoung Yoon , Minki Cho , Jeehoon Kang , Chung-Kil Hur
  OOPSLA, 2025
  [PDF] [DOI]

2024

• Quantum Probabilistic Model Checking for Time-bounded Properties
  Seungmin Jeon , Kyeongmin Cho , Chan Gu Kang , Janggun Lee , Hakjoo Oh , Jeehoon Kang
  OOPSLA, 2024
  [PDF] [DOI]
• A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
  Sunho Park , Jaewoo Kim , Ike Mulder , Jaehwang Jung , Janggun Lee , Robbert Krebbers , Jeehoon Kang
  PLDI, 2024
  [PDF] [DOI]

2023

• Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
  Jaehwang Jung , Janggun Lee , Jaemin Choi , Jaewoo Kim , Sunho Park , Jeehoon Kang
  OOPSLA, 2023
  [PDF] [DOI]
• Applying Hazard Pointers to More Concurrent Data Structures
  Jaehwang Jung , Janggun Lee , Jeonghyeon Kim , Jeehoon Kang
  SPAA, 2023
  [PDF] [DOI]