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
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.
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
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. (conditionally accepted)
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. (accepted)
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.
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).