Hi! I'm Yoonseung Kim. I am an Assistant Professor at DGIST EECS. I was a postdoctoral researcher of the FLINT group in the Computer Science Department at Yale University. I received my PhD from Software Foundations Lab at Seoul National University.

I'm particularly interested in verifying computer systems using the Coq interactive theorem prover. I have been verifying compilers, real-time distributed systems, and consensus protocols.

Contact me via yoonseung.kim at dgist.ac.kr

publication

  • A Formal Verification Library Design for Behavioral Refinement of CompCert Clight
    Yoonseung Kim
    IEEE Access, vol. 13, pp. 26927-26944, 2025
    [paper: url]
  • VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
    Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, Chung-Kil Hur
    Proceedings of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025).
    [paper: pdf]
  • LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
    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 (PLDI 2024).
    [paper: pdf]
  • AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
    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 (OOPSLA 2024).
    [paper: pdf]
  • Formal Verification Framework for Cyber-Physical Systems on PALSware
    Yoonseung Kim
    PhD Thesis, Seoul National University (2021)
    [paper: pdf]
  • 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.
    (* The first three authors contributed equally to this work and are listed alphabetically.)
    Proceedings of the 39th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2018).
    [paper: pdf]
  • Taming Undefined Behavior in LLVM
    Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das (Azul Systems), David Majnemer (Google), John Regehr, Nuno P. Lopes.
    Proceedings of the 38th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2017).
    [paper: pdf]
  • Lightweight Verification of Separate Compilation
    Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
    Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016).
    [paper: pdf]

education

  • Sep. 2013 – Aug. 2021, Ph.D., Computer Science and Engineering, Seoul National University (advisor: Chung-Kil Hur)
  • Feb. 2009 – Feb. 2013, B.S., Computer Science / Mathematical Sciences (double major), magna cum laude (GPA:3.99/4.3), KAIST
  • Mar. 2006 – Feb. 2009, High School Diploma, Korea Science Academy

honors and awards

  • Sep. 2024 - Sep. 2025, Postdoctoral Fellowship Program (Nurturing Next-generation Researchers) granted by National Research Foundation of Korea (NRF)
  • Mar. 2014 – Feb. 2019, EECS Graduate Student Scholarship of Korea Foundation for Advanced Studies (KFAS)
  • Mar. 2009 – Feb. 2013, Korean Presidental Science Scholarship
  • Mar. 2007 – Feb. 2009, KNN Scholarship

professional activities

talks

  • Formal Verification of Middleware for Real-Time Distributed Systems, Mar 2022, KAIST
  • Formal Verification of Middleware for Real-Time Distributed Systems, Feb 2022, KIISE SigPL Winter School 2022
  • Formal Verification of Middleware for Real-Time Distributed Systems, Dec 2021, Yale
  • CreLLVM: Formal Verification of Optimization Passes in LLVM Feb 2019, KIISE SigPL Winter School 2019
  • Lightweight Verification of Separate Compilation Feb 2016, KIISE SigPL Winter Workshop 2016

program committees

research experience

teaching experience

  • TA of Principles of Programming at SNU (4190.210), 2017, 2015, 2014
  • TA of Digital Computer Concept and Practice at SNU (035.001), 2014
  • TA of Automata Theory at SNU (4190.306), 2013
  • Undergraduate TA of Programming Languages at KAIST (CS320), 2012