Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. - Jieung Kim; Sukyoung Ryu (CPP, 2011)

Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance. - Jieung Kim; Sukyoung Ryu; Victor Luchangco; Guy L. Steele Jr. (APLAS, 2013)

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Xiongnan (Newman) Wu; Jieung Kim; Vilhelm Sjöberg; David Costanzo (OSDI, 2016)

Safety and Liveness of MCS Lock - Layer by Layer. - Jieung Kim; Vilhelm Sjöberg; Ronghui Gu; Zhong Shao 001 (APLAS, 2017)

Certified concurrent abstraction layers. - Ronghui Gu; Zhong Shao 001; Jieung Kim; Xiongnan (Newman) Wu; Jérémie Koenig; Vilhelm Sjöberg; Hao Chen 023; David Costanzo; Tahina Ramananandro (PLDI, 2018)

WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. - Ji-Yong Shin; Jieung Kim; Wolf Honoré; Hernán Vanzetto; Srihari Radhakrishnan; Mahesh Balakrishnan 001; Zhong Shao 001 (SoCC, 2019)

Building certified concurrent OS kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Jieung Kim; Jérémie Koenig; Xiongnan (Newman) Wu; Vilhelm Sjöberg; David Costanzo (Commun. ACM, 2019)

Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. - Wolf Honoré; Jieung Kim; Ji-Yong Shin; Zhong Shao 001 (Proc. ACM Program. Lang., 2021)

Adore: atomic distributed objects with certified reconfiguration. - Wolf Honoré; Ji-Yong Shin; Jieung Kim; Zhong Shao 001 (PLDI, 2022)

Towards Efficient Formal Verification of Spiking Neural Network. - Baekryun Seong; Jieung Kim; Sang-Ki Ko (CoRR, 2024)

MPruner: Optimizing Neural Network Size with CKA-Based Mutual Information Pruning. - Seungbeom Hu; ChanJun Park; Andrew Ferraiuolo; Sang-Ki Ko; Jinwoo Kim; Haein Song; Jieung Kim (CoRR, 2024)

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. - Wolf Honoré; Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. - Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Wolf Honoré; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification. - Jieung Kim; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)

ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions. - Jieung Kim; Jérémie Koenig; Hao Chen 023; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)

ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol. - Kezhi Xiong; Soonwon Moon; Joshua H. Kang; Bryant Curto; Jieung Kim; Ji-Yong Shin (DSN, 2025)