Juneyoung Lee (이준영, June Lee), Ph.D.

I am a Senior Applied Scientist at Automated Reasoning Group in AWS (Austin, TX). I work on writing a provably correct code that is also fast.

I received Ph.D. from Software Foundations Lab, Seoul National University in August, 2021.

• E-mail: lebjuney@amazon.com, aqjune@gmail.com (personal), juneyoung.lee@sf.snu.ac.kr (old)
• Google scholar: scholar.google.com/citations?user=ROTPVwkAAAAJ&hl=ko
• ORCID: 0000-0002-8152-9330

News

• Apr. 13, 2026: A paper “Towards Removing Undef Values From LLVM IR” was accepted to PLDI’26!
• Apr. 9, 2026: A workshop talk “s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs” was accepted to AIPV’26!

Interests

• Programming languages, compiler verification
• Theorem proving using SMT solvers and interactive theorem provers
• Verification of cryptographic libraries

Awards, Activities and Experience

• Go to my activities and experience

Publications

• Go to the publications page or Google Scholar

Education

• Ph.D. in Computer Science and Engineering, Seoul National University (2016. Mar ~ 2021. Aug)
  • Advisors: Chung-Kil Hur, Nuno. P. Lopes.
  • Thesis: A Validated Semantics for LLVM IR
    • Recipient of Best Thesis Award from College of Engineering, SNU (one thesis chosen per dept.)
• B.S. in Computer Science and Engineering, minor in Life Science, POSTECH, magna cum laude (~ 2014. 8)

Blog Posts

• Mar. 20, 2026. Formally verified AES-XTS: The first AES algorithm to join s2n-bignum
• Aug. 8, 2024. Formal verification makes RSA faster — and faster to deploy
• Oct. 4, 2021. The select story