| {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 | 309 | 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 | 47 | 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 | 36 | 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 | 32 | 2017 |
| 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 | 11 | 2022 |
| 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 | 10 | 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 | 8 | 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 | 3 | 2011 |
| 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 | 1 | 2013 |
| Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness J Kim, S Ryu Technical Report ROSAEC-2011-011, KAIST (May 2011), 2011 | 1 | 2011 |
| 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 |
