Jieung Kim
Cited by
Cited by
{CertiKOS}: An Extensible Architecture for Building Certified Concurrent {OS} Kernels
R Gu, Z Shao, H Chen, XN Wu, J Kim, V Sjöberg, D Costanzo
12th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2016
Certified concurrent abstraction layers
R Gu, Z Shao, J Kim, X Wu, J Koenig, V Sjöberg, H Chen, D Costanzo, ...
ACM SIGPLAN Notices 53 (4), 646-661, 2018
Building certified concurrent OS kernels
R Gu, Z Shao, H Chen, J Kim, J Koenig, X Wu, V Sjöberg, D Costanzo
Communications of the ACM 62 (10), 89-99, 2019
Safety and liveness of MCS lock—layer by layer
J Kim, V Sjöberg, R Gu, Z Shao
Programming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou …, 2017
Wormspace: a modular foundation for simple, verifiable distributed systems
JY Shin, J Kim, W Honoré, H Vanzetto, S Radhakrishnan, M Balakrishnan, ...
Proceedings of the ACM Symposium on Cloud Computing, 299-311, 2019
Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems
W Honoré, J Kim, JY Shin, Z Shao
Proceedings of the ACM on Programming Languages 5 (OOPSLA), 1-31, 2021
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance
J Kim, S Ryu
Certified Programs and Proofs: First International Conference, CPP 2011 …, 2011
Adore: atomic distributed objects with certified reconfiguration
W Honoré, JY Shin, J Kim, Z Shao
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022
Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance
J Kim, S Ryu, V Luchangco, GL Steele
Programming Languages and Systems: 11th Asian Symposium, APLAS 2013 …, 2013
Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness
J Kim, S Ryu
Technical Report ROSAEC-2011-011, KAIST (May 2011), 2011
Proving FFMM type safety using coq
K Ji-Eung
한국과학기술원, 2011
The system can't perform the operation now. Try again later.
Articles 1–11