Juneyoung Lee (이준영). Ph.D.
Software Foundations Lab, Seoul National University.
Advisors : Prof. Chung-Kil Hur, Nuno. P. Lopes.
NOTE: I graduated in August 2021 and moved to CryptoLab. This page will not be updated anymore.
https://aqjune.github.io/ is my new web site.

Education

  • Ph.D. in Computer Science and Engineering, Seoul National University(2016. Mar ~ 2021. Aug)
  • 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

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

Publication

  1. An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation.
    Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes.
    33rd International Conference on Computer-Aided Verification (CAV 2021). (link)
  2. Alive2: Bounded Translation Validation for LLVM.
    Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr.
    In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021) (link).
    Recipient of PLDI 2021 Distinguished Paper Award.
  3. 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)
  4. 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)
  5. 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 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). (link)
    * The first three authors contributed equally to this work and are listed alphabetically.
  6. 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 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). (link)
  7. DualSim: Parallel Subgraph Enumeration in a Massive Graph on a Single Machine
    Hyeonji Kim, Juneyoung Lee, Sourav S. Bhowmick, Wook-Shin Han, JeongHoon Lee, Seongyun Ko, and Moath H.A. Jarrah
    In Proceedings of the 42nd ACM SIGMOD/PODS International Conference on Management of Data (SIGMOD 2016).

Professional Activities

  • Talks:
    • "Undef and Poison: Present and Future", The 2020 Virtual LLVM Developers' Meeting, Keynote Talk  (link)
    • "Safely Optimizing Casts between Pointers and Integers": 2019 European LLVM developers' meeting, Student Research Competition, Second Prize
  • CAV 2020, Artifact Evaluation Committee
  • ICFP 2020, Student Volunteer

Experience

Awards and Honors