Juneyoung Lee

Logo

View My GitHub Profile

Publications

  1. Towards Removing Undef Values From LLVM IR.
    Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, Nuno P. Lopes.
    PLDI 2026.
  2. Relational Hoare Logic for Realistically Modelled Machine Code.
    Denis Mazzucato*, Abdalrhman Mohamed*, Juneyoung Lee†, Clark Barrett, Jim Grundy, John Harrison, Corina Pasareanu.
    CAV 2025. (doi)
    - The first two authors contributed equally to the paper.
  3. Optimization-Directed Compiler Fuzzing for Continuous Translation Validation.
    Jaeseong Kwon, Bongjun Jang, Juneyoung Lee, and Kihong Heo.
    PLDI 2025. (doi)
  4. Translation Validation for JIT Compiler in the V8 JavaScript Engine.
    Seungwan Kwon, Jaeseong Kwon, Wooseok Kang, Juneyoung Lee, Kihong Heo.
    ICSE 2024. (doi)
  5. HEaaN.MLIR: An Optimizing Compiler for Fast Ring-Based Homomorphic Encryption.
    Sunjae Park*, Woosung Song*, Seunghyeon Nam, Hyeongyu Kim, Junbum Shin, Juneyoung Lee†.
    PLDI 2023. (doi)
    - The first two authors contributed equally to the paper.
    - Two authors (S. Park, H. Kim) were undergraduate students when the paper was submitted!
  6. SMT-based Translation Validation for Machine Learning Compiler.
    Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, Juneyoung Lee†.
    CAV 2022. (doi)
    https://github.com/aqjune/mlir-tv
    - Two authors (S. Bang and I. Chun) were undergraduate students when the paper was submitted!
  7. An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation.
    Juneyoung Lee, D. Kim, C-K. Hur, N. P. Lopes.
    CAV 2021. (doi)
  8. Alive2: Bounded Translation Validation for LLVM.
    N. P. Lopes, Juneyoung Lee, C-K. Hur, Z. Liu, J. Regehr.
    PLDI 2021. (doi)
    https://alive2.llvm.org , https://github.com/AliveToolkit/alive2/
    Recipient of Distinguished Paper Award.
  9. AliveInLean: A Verified LLVM Peephole Optimization Verifier.
    Juneyoung Lee, C-K. Hur, N. P. Lopes.
    CAV 2019, Tool Paper. (doi)
    https://github.com/microsoft/aliveinlean
  10. Reconciling High-level Optimizations and Low-level Code in LLVM.
    Juneyoung Lee, C-K. Hur, R. Jung, Z. Liu, J. Regehr, N. P. Lopes.
    OOPSLA 2018. (doi)
    https://sf.snu.ac.kr/llvmtwin
  11. Crellvm: Verified Credible Compilation for LLVM.
    J. Kang*, Y. Kim*, Y. Song*, Juneyoung Lee, S. Park, M. D. Shin, Y. Kim, S. Cho, J. Choi, C-K. Hur, K. Yi.
    PLDI 2018. (doi)
    https://sf.snu.ac.kr/crellvm
  12. Taming Undefined Behavior in LLVM.
    Juneyoung Lee, Y. Kim, Y. Song, C-K. Hur, S. Das, D. Majnemer, J. Regehr, N. P. Lopes.
    PLDI 2017. (doi)
    https://sf.snu.ac.kr/freeze
  13. DualSim: Parallel Subgraph Enumeration in a Massive Graph on a Single Machine.
    H. Kim, Juneyoung Lee, S. S. Bhowmick, W-S. Han, J. Lee, S. Ko, and M. H.A. Jarrah.
    SIGMOD 2016. (doi)