| Taming undefined behavior in LLVM J Lee, Y Kim, Y Song, CK Hur, S Das, D Majnemer, J Regehr, NP Lopes ACM SIGPLAN Notices 52 (6), 633-647, 2017 | 77 | 2017 |
| Crellvm: verified credible compilation for LLVM J Kang, Y Kim, Y Song, J Lee, S Park, MD Shin, Y Kim, S Cho, J Choi, ... Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018 | 38 | 2018 |
| CompCertM: CompCert with C-assembly linking and lightweight modular verification Y Song, M Cho, D Kim, Y Kim, J Kang, CK Hur Proceedings of the ACM on Programming Languages 4 (POPL), 1-31, 2019 | 36 | 2019 |
| Conditional Contextual Refinement Y Song, M Cho, D Lee, CK Hur, M Sammler, D Dreyer Proceedings of the ACM on Programming Languages 7 (POPL), 1121-1151, 2023 | 16 | 2023 |
| DimSum: A decentralized approach to multi-language semantics and verification M Sammler, S Spies, Y Song, E D'Osualdo, R Krebbers, D Garg, D Dreyer Proceedings of the ACM on Programming Languages 7 (POPL), 775-805, 2023 | 14 | 2023 |
| Fair Operational Semantics D Lee, M Cho, J Kim, S Moon, Y Song, CK Hur Proceedings of the ACM on Programming Languages 7 (PLDI), 811-834, 2023 | 3 | 2023 |
| Stuttering for Free M Cho, Y Song, D Lee, L Gäher, D Dreyer Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 1677-1704, 2023 | | 2023 |
| Conditional Contextual Refinement (CCR) Y Song, M Cho, D Lee, CK Hur arXiv preprint arXiv:2203.07431, 2022 | | 2022 |
| Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic Y Song, M Cho, D Lee, CK Hur arXiv preprint arXiv:2109.02991, 2021 | | 2021 |
| Appendix of DimSum: A Decentralized Approach to Multi-language Semantics and Verification M SAMMLER, S SPIES, Y SONG, E D’OSUALDO, D GARG, D DREYER | | |
