A Dice Rolling Game on a Set of Tori. - Jeehoon Kang; Suh-Ryung Kim; Boram Park (Electron. J. Comb., 2012)

Global Sparse Analysis Framework. - Hakjoo Oh; Kihong Heo; Wonchan Lee; Woosuk Lee; Daejun Park 001; Jeehoon Kang; Kwangkeun Yi (ACM Trans. Program. Lang. Syst., 2014)

A formal C memory model supporting integer-pointer casts. - Jeehoon Kang; Chung-Kil Hur; William Mansky; Dmitri Garbuzov; Steve Zdancewic; Viktor Vafeiadis (PLDI, 2015)

Lightweight verification of separate compilation. - Jeehoon Kang; Yoonseung Kim; Chung-Kil Hur; Derek Dreyer; Viktor Vafeiadis (POPL, 2016)

Repairing sequential consistency in C/C++11. - Ori Lahav 001; Viktor Vafeiadis; Jeehoon Kang; Chung-Kil Hur; Derek Dreyer (PLDI, 2017)

A promising semantics for relaxed-memory concurrency. - Jeehoon Kang; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis; Derek Dreyer (POPL, 2017)

Crellvm: verified credible compilation for LLVM. - Jeehoon Kang; Yoonseung Kim; Youngju Song; Juneyoung Lee; Sanghoon Park; Mark Dongyeon Shin; Yonghyun Kim; Sungkeun Cho; Joonwon Choi; Chung-Kil Hur; Kwangkeun Yi (PLDI, 2018)

Promising-ARM/RISC-V: a simpler and faster operational concurrency model. - Christopher Pulte; Jean Pichon-Pharabod; Jeehoon Kang; Sung-Hwan Lee 001; Chung-Kil Hur (PLDI, 2019)

Enveloping Implicit Assumptions of Intrusive Data Structures within Ownership Type System. - Keunhong Lee; Jeehoon Kang; Wonsup Yoon; Joongi Kim; Sue B. Moon (PLOS@SOSP, 2019)

A marriage of pointer- and epoch-based reclamation. - Jeehoon Kang; Jaehwang Jung (PLDI, 2020)

Stacked borrows: an aliasing model for Rust. - Ralf Jung 002; Hoang-Hai Dang; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2020)

CompCertM: CompCert with C-assembly linking and lightweight modular verification. - Youngju Song; Minki Cho; Dongjoo Kim; Yonghyun Kim; Jeehoon Kang; Chung-Kil Hur (Proc. ACM Program. Lang., 2020)

Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8. - Kyeongmin Cho; Sung-Hwan Lee 001; Azalea Raad; Jeehoon Kang (PLDI, 2021)

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 (PLDI, 2022)

Practical Detectability for Persistent Lock-Free Data Structures. - Kyeongmin Cho; Seungmin Jeon; Jeehoon Kang (CoRR, 2022)

Continuous verification of system of systems with collaborative MAPE-K pattern and probability model slicing. - Jiyoung Song; Jeehoon Kang; Sangwon Hyun; Eunkyoung Jee; Doo-Hwan Bae (Inf. Softw. Technol., 2022)

Simuliris: a separation logic framework for verifying concurrent program optimizations. - Lennard Gäher; Michael Sammler; Simon Spies; Ralf Jung 002; Hoang-Hai Dang; Robbert Krebbers; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Forecasting Obsolescence of Components by Using a Clustering-Based Hybrid Machine-Learning Algorithm. - Kyoung-Sook Moon; Hee Won Lee; Hee Jean Kim; Hongjoong Kim; Jeehoon Kang; Won Chul Paik (Sensors, 2022)

ShakeFlow: Functional Hardware Description with Latency-Insensitive Interface Combinators. - Sungsoo Han; Minseong Jang; Jeehoon Kang (ASPLOS (2), 2023)

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

Memento: A Framework for Detectable Recoverability in Persistent Memory. - Kyeongmin Cho; Seungmin Jeon; Azalea Raad; Jeehoon Kang (Proc. ACM Program. Lang., 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)

Concurrent Immediate Reference Counting (Abstract). - Jaehwang Jung; Jeonghyeon Kim; Matthew J. Parkinson; Jeehoon Kang (HOPC@SPAA, 2024)

Expediting Hazard Pointers with Bounded RCU Critical Sections. - Jeonghyeon Kim; Jaehwang Jung; Jeehoon Kang (SPAA, 2024)

Modular Hardware Design of Pipelined Circuits with Hazards. - Minseong Jang; Jungin Rhee; Woojin Lee; Shuangshuang Zhao; Jeehoon Kang (Proc. ACM Program. Lang., 2024)

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)

Concurrent Immediate Reference Counting. - Jaehwang Jung; Jeonghyeon Kim; Matthew J. Parkinson; 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)