Conference

2024
  • Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honore, and Zhong Shao, LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs Proceedings of 2024 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'24), June 2024.
  • Wolf Honore, Longfei Qiu, Ji-Yong Shin, Yoonseung Kim, Jieung Kim, and Zhong Shao, AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects Proceedings of 2024 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'24), October 2024.

  • 2022
  • 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.

  • 2021
  • 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)

  • Before 2020
  • 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.
  • Journal

    2024
  • Jieung Kim, Jeremie Koenig, Hao Chen, Ronghui Gu, and Zhong Shao, ThreadAbs: A Template for Building Verified Thread-local Interfaces with Software Scheduler Abstractions Journal of Systems Architecture, Volume 147, Article 103046, February 2024.
  • Jieung Kim, Ronghui Gu, and Zhong Shao, SimplMM: A Simplified and Abstract Multicore Hardware Model for Large Scale System Software Formal Verification Journal of Systems Architecture, Volume 147, Article 103046, February 2024.

  • Before 2020
  • 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.
  • 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.
  • Domestic Journal and Conference

  • 김지응, 정형 검증을 통한 동시성 소프트웨어의 추상화 명세 제공 (Provide abstracted specifications for concurrent software with formal verification) 정보과학회지 제41권 제6호(통권 제409호), June 2023.
  • Working Papers

  • Kezhi Xiong, Soonwon Moon, Joshua Hankyul Kang, Bryant Curto, Jieung Kim, and Ji-Yong Shin, ReCraft: Split, Merge, and Membership Change of Raft in etcd, (in review).
  • 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)
  • © Jieung Kim. All Rights Reserved. Designed by HTML Codex