[Google Scholar | DBLP]

Thesis

Jieung Kim (Yale University), Modular and Compositional Development of Certified Concurrent Software Systems (Ph.D. Thesis)

Jieung Kim (KAIST), Proving FFMM Type Safety Using Coq (MS Thesis)

Journal

Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jeremie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjoberg, and David Costanzo, Building Certified Concurrent OS Kernels, Communications of the ACM, 62(10), pages 89-99, October 2019.

Conference

Wolf Honore, Ji-Yong Shin, Jieung Kim*, and Zhong Shao , Adore: Atomic Distributed Objects with Certified Reconfiguration Proceedings of 2022 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'22), June 2022.

Wolf Honore*, Jieung Kim*, Ji-Yong Shin, and Zhong Shao , Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems Proceedings of 2021 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'21), October 2021. (*: both equally contribute to this work)

Ji-Yong Shin, Jieung Kim, Wolf Honore, Hernan Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, and Zhong Shao , WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems, ACM Symposium on Cloud Computing 2019 (SoCC ’19), November 2019.

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jeremie Koenig, Vilhelm Sjoberg, Hao Chen, David Costanzo, and Tahina Ramananandro, Certified Concurrent Abstraction Layers, Proceedings of 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2018.

Jieung Kim, Vilhelm Sjoberg, Ronghui Gu, and Zhong Shao, Safety and Liveness of MCS Lock—Layer by Layer, Proceedings of the 15th Asian Symposium on Programming Languages and Systems, November 2017.

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjoberg, and David Costanzo, CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels, 12th 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, 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, December 2011.

Poster

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jeremie Koenig, Vilhelm Sjoberg, Hao Chen, David Costanzo, and Tahina Ramananandro, Certified Concurrent Abstraction Layers, Proceedings of 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2018.

Technical Report

Ji-Yong Shin, Jieung Kim, Wolf Honore, Hernan Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, and Zhong Shao, Write-Once-Registers: A Modular Foundation for Simple, Verifiable Distributed Systems, Technical report - YALEU/DCS/TR1544, December 2018

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

Working Papers

Wolf Honore, Ji-Yong Shin, Longfei Qiu, Yoonseung Kim, Jieung Kim*, and Zhong Shao , AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects

Jieung Kim*, Jeremie Koenig, Ronghui Gu, and Zhong Shao , Multicore Semantics and Linking in CertiKOS

Jieung Kim*, Jeremie Koenig, Ronghui Gu, and Zhong Shao , Multithread Semantics and Linking in CertiKOS