Applying Hazard Pointers to More Concurrent Data Structures. - Jaehwang Jung; Janggun Lee; Jeonghyeon Kim; Jeehoon Kang (SPAA, 2023)

Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic. - Jaehwang Jung; Janggun Lee; Jaemin Choi; Jaewoo Kim; Sunho Park; Jeehoon Kang (Proc. ACM Program. Lang., 2023)

Quantum Probabilistic Model Checking for Time-Bounded Properties. - Seungmin Jeon; Kyeongmin Cho; Chan Gu Kang; Janggun Lee; Hakjoo Oh; Jeehoon Kang (Proc. ACM Program. Lang., 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 (Proc. ACM Program. Lang., 2024)

Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic. - Jaehwang Jung; Sunho Park; Janggun Lee; Jeho Yeon; Jeehoon Kang (Proc. ACM Program. Lang., 2025)

Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals. - Janggun Lee; Jeonghyeon Kim; Jeehoon Kang (Proc. ACM Program. Lang., 2025)

Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness. - Dongjae Lee; Janggun Lee; Taeyoung Yoon; Minki Cho; Jeehoon Kang; Chung-Kil Hur (Proc. ACM Program. Lang., 2025)

Verifying Lock-Free Traversals in Relaxed Memory Separation Logic. - Sunho Park; Jaehwang Jung; Janggun Lee; Jeehoon Kang (Proc. ACM Program. Lang., 2025)