• A Formal Verification Library Design for Behavioral Refinement of CompCert Clight [IEEE Access, 2025]
    Yoonseung Kim. IEEE Access, vol. 13, pp. 26927-26944, 2025
    Official Link
  • VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems [POPL 2025]
    Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, Chung-Kil Hur. Proceedings of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages"
    Official Link Local Copy
  • LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs [PLDI 2024]
    Longfei Qiu, Yoonseung Kim, Ji-Yoon Shin, Jieung Kim, Wolf Honore, and Zhong Shao. Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation
    Official Link
  • AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects [OOPSLA 2024]
    Wolf Honore, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Zhong Shao. Proceedings of 2024 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
    Official Link
  • Crellvm: Verified Credible Compilation for LLVM [PLDI 2018]
    Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi. Proceedings of the 39th annual ACM SIGPLAN conference on Programming Languages Design and Implementation
    Official Link
  • Taming Undefined Behavior in LLVM [PLDI 2017]
    Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, Nuno P. Lopes. Proceedings of the 38th annual ACM SIGPLAN conference on Programming Languages Design and Implementation
    Offical Link
  • Lightweight Verification of Separate Compilation [POPL 2016]
    Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis. Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    Official Link