Research Interests

• Software Verification
• Compiler Verification
• Hardware Verification

Publications

• CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
  Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, Chung-Kil Hur
  In Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).
  [project page]

• 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).
  [draft paper: pdf] [development: zip]

• 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] [project page]

Education

• Mar. 2015 – Feb. 2021, Ph.D. Computer Science and Engineering, Seoul National University (advisor: Chung-Kil Hur)
• Thesis: RUSC and CompCertM: A new foundation for modular verification and its application to compiler verification
• Feb. 2010 – Feb. 2015, B.S., Computer Science & Mathematical Sciences (double major), KAIST
• Mar. 2007 – Feb. 2010, Korea Science Academy

Experience

• Exchange Student. Tokyo Institute of Technology. 2012 June ~ 2012 July (advisor: Kazuyuki Shudo)
• Research Assistant Intern. Frograms, Inc. 2013 March ~ 2013 June

Honors and Awards

• Gold medal in the 23th Korean Mathematical Olympiad (KMO) first round, 2009
• 5th place in ACM International Collegiate Programming Contest (ICPC) regional, 2012
• 2nd place in ACM International Collegiate Programming Contest (ICPC) regional first round, 2013