Taming undefined behavior in LLVM. - Juneyoung Lee; Yoonseung Kim; Youngju Song; Chung-Kil Hur; Sanjoy Das; David Majnemer; John Regehr; Nuno P. Lopes (PLDI, 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)

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)

Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic. - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur (CoRR, 2021)

Conditional Contextual Refinement (CCR). - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur (CoRR, 2022)

Fair Operational Semantics. - Dongjae Lee; Minki Cho; Jinwoo Kim; Soonwon Moon; Youngju Song; Chung-Kil Hur (Proc. ACM Program. Lang., 2023)

DimSum: A Decentralized Approach to Multi-language Semantics and Verification. - Michael Sammler; Simon Spies; Youngju Song; Emanuele D'Osualdo; Robbert Krebbers; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Conditional Contextual Refinement. - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur; Michael Sammler; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Stuttering for Free. - Minki Cho; Youngju Song; Dongjae Lee; Lennard Gäher; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Refinement Composition Logic. - Youngju Song; Dongjae Lee (Proc. ACM Program. Lang., 2024)

Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting. - Yonghyun Kim; Minki Cho; Jaehyung Lee; Jinwoo Kim; Taeyoung Yoon; Youngju Song; Chung-Kil Hur (Proc. ACM Program. Lang., 2025)

CCR 2.0: High-level Reasoning for Conditional Refinements. - Youngju Song; Minki Cho (CoRR, 2025)