About

 

I'm a Ph.D candidate in FLINT Group at the Department of Computer Science of Yale University, and my advisor is Zhong Shao. I received a M.S. in Computer Science from KAIST, and B.S.E in School of Information and Communication Enginnering from Sungkyunkwan University. AS a M.S. thesis, I worked on building a type system for a small object oriented program language with Professor Sukyoung Ryu, who is a PI of PLRG in KAIST.

Research Interest

 

  • Operating System Design
  • Concurrent Object Verification
  • Software Verification
  • Information Flow Control
  • Proof Assistants and Automated Proof

 

 

Education

 

  • Ph.D Candidacy in Computer Science, September 2012 - Present,

Computer Science Department, Yale

 

  • M.S. in Computer Science, September 2009 - August 2011,

Computer Science Department, KAIST

Thesis: Proving FFMM Type Safety Using Coq

Advisor: Sukyoung Ryu

 

  • B.S.E. in Computer Engineering, March 2002 - August 2009,

School of Information and Communication Engineering, SKKU

 

 

Work Experience

 

  • Assistant in Research, September 2011 - August 2012

Computer Science Department, KAIST

 

 

Publications

 

  • Ronghui Gu, Zhong Shao, Hao Chen, Newman Wu, Jieung Kim, Vilhelm Sjoberg, David Costanzo, "CertiKOS: An Extenisble Architecture for Building Certified Concurrent OS Kernels (Research Paper)," In Proc. 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), November 2016.

 

  • Ronghui Gu, Zhong Shao, Hao Chen, Newman Wu, Jieung Kim, Vilhelm Sjoberg, David Costanzo, "CertiKOS: An Extenisble Architecture for Building Certified Concurrent OS Kernels (Poster)," In Proc. 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), November 2016.

 

  • Jieung Kim, Sukyoung Ryu, Victor Luchangco, and Guy L. Steele Jr., "Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance," Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS'13), December 2013.

 

  • Jieung Kim and Sukyoung Ryu, "Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance," The First International Conference on Certified Programs and Proofs (CPP'11), December 2011.

 

  • Jieung Kim, "Proving FFMM Type Safety Using Coq," Master's Thesis (Awarded as an Outstanding M.S. thesis of the year), Korea Advanced Institute of Science and Technology, August 2011.

 

  • Jieung Kim and Sukyoung Ryu, "Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness," Technical Report (ROSAEC-2011-011), May 2011.

 

 

Contacts

 

  • E-mail

jieung.kim [at] yale.edu

 

  • Address

Room 311

Computer Science Department

51 Prospect Street (AKW) New Haven

CT, U.S.A 06511