| Repairing sequential consistency in C/C++ 11 O Lahav, V Vafeiadis, J Kang, CK Hur, D Dreyer ACM SIGPLAN Notices 52 (6), 618-632, 2017 | 240 | 2017 |
| A promising semantics for relaxed-memory concurrency J Kang, CK Hur, O Lahav, V Vafeiadis, D Dreyer ACM SIGPLAN Notices 52 (1), 175-189, 2017 | 231 | 2017 |
| Interaction trees: representing recursive and impure programs in Coq L Xia, Y Zakowski, P He, CK Hur, G Malecha, BC Pierce, S Zdancewic Proceedings of the ACM on Programming Languages 4 (POPL), 1-32, 2019 | 153 | 2019 |
| Biorthogonality, step-indexing and compiler correctness N Benton, CK Hur ACM Sigplan Notices 44 (9), 97-108, 2009 | 140 | 2009 |
| R2: An efficient MCMC sampler for probabilistic programs A Nori, CK Hur, S Rajamani, S Samuel Proceedings of the AAAI Conference on Artificial Intelligence 28 (1), 2014 | 138 | 2014 |
| The power of parameterization in coinductive proof CK Hur, G Neis, D Dreyer, V Vafeiadis Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013 | 134 | 2013 |
| Strongly typed term representations in Coq N Benton, CK Hur, AJ Kennedy, C McBride Journal of automated reasoning 49 (2), 141-159, 2012 | 115 | 2012 |
| A Kripke logical relation between ML and assembly CK Hur, D Dreyer Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2011 | 115 | 2011 |
| Pilsner: A compositionally verified compiler for a higher-order imperative language G Neis, CK Hur, JO Kaiser, C McLaughlin, D Dreyer, V Vafeiadis Proceedings of the 20th ACM SIGPLAN International Conference on Functional …, 2015 | 102 | 2015 |
| The marriage of bisimulations and Kripke logical relations CK Hur, D Dreyer, G Neis, V Vafeiadis ACM SIGPLAN Notices 47 (1), 59-72, 2012 | 100 | 2012 |
| Alive2: bounded translation validation for LLVM NP Lopes, J Lee, CK Hur, Z Liu, J Regehr Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021 | 91 | 2021 |
| 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 | 86 | 2017 |
| Second-order equational logic M Fiore, CK Hur Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual …, 2010 | 83 | 2010 |
| Lightweight verification of separate compilation J Kang, Y Kim, CK Hur, D Dreyer, V Vafeiadis Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2016 | 75 | 2016 |
| A formal C memory model supporting integer-pointer casts J Kang, CK Hur, W Mansky, D Garbuzov, S Zdancewic, V Vafeiadis ACM SIGPLAN Notices 50 (6), 326-335, 2015 | 71 | 2015 |
| Slicing probabilistic programs CK Hur, AV Nori, SK Rajamani, S Samuel ACM SIGPLAN Notices 49 (6), 133-144, 2014 | 63 | 2014 |
| Promising 2.0: global optimizations in relaxed memory concurrency SH Lee, M Cho, A Podkopaev, S Chakraborty, CK Hur, O Lahav, ... Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020 | 57 | 2020 |
| Promising-ARM/RISC-V: a simpler and faster operational concurrency model C Pulte, J Pichon-Pharabod, J Kang, SH Lee, CK Hur Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019 | 56 | 2019 |
| On the construction of free algebras for equational systems M Fiore, CK Hur Theoretical Computer Science 410 (18), 1704-1729, 2009 | 44 | 2009 |
| 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 | 40 | 2019 |
Viktor VafeiadisMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics Campus (SIC)Verified email at mpi-sws.org
