Publications
-
Translation Validation for JIT Compiler in the V8 JavaScript Engine.
Seungwan Kwon, Jaeseong Kwon, Wooseok Kang, Juneyoung Lee, Kihong Heo.
ICSE 2024. (doi)
-
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!
-
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!
-
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)
-
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.
-
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
-
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
-
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
-
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
-
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)
- Thesis: A Validated Semantics for LLVM IR. (link)