Yoonseung Kim

publication

• VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
  Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, Chung-Kil Hur
  (To Appear) Proceedings of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025).
  [list of accepted papers]
• 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
  [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

• PC (CPP 2023), SRC (POPL 2023), AEC (POPL 2020)

research experience

• Sep. 2024 - Current, Lab Associate, FLINT group, Yale University
• Jun. 2022 - Aug. 2024, Postdoctoral Associate, FLINT group, Yale University
• Sep. 2021 - May. 2022, Postdoctoral Fellow, Software Foundations Lab, Seoul National University
• 2011 - 2012, Undergraduate Researcher, Programming Language Research Group, KAIST

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