Follow
Jieung Kim
Title
Cited by
Cited by
Year
{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
2892016
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
462018
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
342019
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
292017
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
102019
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
42022
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
32021
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
32011
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
12013
Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness
J Kim, S Ryu
Technical Report ROSAEC-2011-011, KAIST (May 2011), 2011
12011
SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification
J Kim, R Gu, Z Shao
Journal of Systems Architecture 147, 103049, 2024
2024
ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions
J Kim, J Koenig, H Chen, R Gu, Z Shao
Journal of Systems Architecture 147, 103046, 2024
2024
Proving FFMM type safety using coq
K Ji-Eung
한국과학기술원, 2011
2011
The system can't perform the operation now. Try again later.
Articles 1–13