Conference
2026
-
PLDI
2026CRIS: The Power of Imagination in Hybrid Verification
Proceedings of the 2026 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’26), June 2026. Proc. ACM Program. Lang. 10, PLDI, Article 239.
2025
-
DSN
2025ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol
The 55th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN’25), June 2025.
2024
-
PLDI
2024LiDO: 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.
-
OOPSLA
2024AdoB: 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
-
PLDI
2022Adore: Atomic Distributed Objects with Certified Reconfiguration
Proceedings of 2022 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’22), June 2022.
2021
-
OOPSLA
2021Proceedings 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
-
SoCC
2019WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems
ACM Symposium on Cloud Computing 2019 (SoCC’19), November 2019.
-
PLDI
2018Certified Concurrent Abstraction Layers
Proceedings of 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2018.
-
APLAS
2017Safety and Liveness of MCS Lock—Layer by Layer
Proceedings of the 15th Asian Symposium on Programming Languages and Systems, November 2017.
-
OSDI
2016CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels
12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), November 2016.
-
APLAS
2013Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance
Proceedings of the 11th Asian Symposium on Programming Languages and Systems, December 2013.
-
CPP
2011Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance
The First International Conference on Certified Programs and Proofs, December 2011.
Workshop
-
PLOS
2025Compositional Model-Driven Verification of Weakly Consistent Distributed Systems
Proceedings of the 13th Workshop on Programming Languages and Operating Systems (PLOS’25), October 2025.
Journal
-
JSA
2024Journal of Systems Architecture, Volume 147, Article 103046, February 2024.
-
JSA
2024Journal of Systems Architecture, Volume 147, Article 103046, February 2024.
-
CACM
2019Building Certified Concurrent OS Kernels
Communications of the ACM, 62(10), pages 89–99, October 2019.
Technical Report
-
TR
2018Write-Once-Registers: A Modular Foundation for Simple, Verifiable Distributed Systems
Technical report — YALEU/DCS/TR1544, December 2018.
-
TR
2011Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness
Technical Report (ROSAEC-2011-011), May 2011.
Domestic Journal and Conference
-
KIISE
2023정형 검증을 통한 동시성 소프트웨어의 추상화 명세 제공 (Provide abstracted specifications for concurrent software with formal verification)
정보과학회지 제41권 제6호(통권 제409호), June 2023.
Working Papers
-
In
reviewReCraft: Split, Merge, and Membership Change of Raft in etcd
(in review)
Thesis
-
Ph.D
YaleModular and Compositional Development of Certified Concurrent Software Systems
Ph.D. Thesis
-
MS
KAISTProving FFMM Type Safety Using Coq
MS Thesis