Juneyoung Lee (이준영)
Software Foundations Lab, Seoul National University.
advisor : Prof. Chung-Kil Hur.
I'm contributing to LLVM project and Alive2 (alive2.llvm.org)


  • Ph.D. in Computer Science and Engineering, Seoul National University(2016. Mar ~ now)
  • B.S. in Computer Science and Engineering, minor in Life Science, POSTECH, magna cum laude (~ 2014. 8)
  • High school diploma, Daegu Science High School (~ 2010. 2)

Research Interest

  • Formal semantics of programming languages
  • Compiler verification using SMT solver and interactive theorem prover


  1. AliveInLean: A Verified LLVM Peephole Optimization Verifier.
    Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes.
    31st International Conference on Computer-Aided Verification (CAV 2019), Tool Paper. (link)
  2. Reconciling High-level Optimizations and Low-level Code in LLVM.
    Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes.
    The 2018 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2018). (link)
  3. Crellvm: Verified Credible Compilation for LLVM
    Jeehoon Kang*, Yoonseung Kim*, Youngju Song*, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur**, Kwangkeun Yi.
    In Proceedings of the 39th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2018). (link)
    * The first three authors contributed equally to this work and are listed alphabetically.
  4. Taming Undefined Behavior in LLVM
    Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das (Azul Systems), David Majnemer (Google), John Regehr, Nuno P. Lopes.
    In Proceedings of the 38th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2017). (link)
  5. DualSim: Parallel Subgraph Enumeration in a Massive Graph on a Single Machine
    Kim, H., Lee, J., Bhowmick, S., Han, W., Lee, J., Ko, S., and Jarrah, M.
    In Proc. 42nd Int’l conf. on Management of Data, ACM SIGMOD, San Francisco, USA, June 2016.


Awards and Honors

Professional Activities