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

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)

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. - Wolf Honoré; Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. - Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Wolf Honoré; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

A Formal Verification Library Design for Behavioral Refinement of CompCert Clight. - Yoonseung Kim (IEEE Access, 2025)

VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems. - Yoonseung Kim; Sung-Hwan Lee 001; Yonghyun Kim; Chung-Kil Hur (Proc. ACM Program. Lang., 2025)