I am an Applied Scientist at Automated Reasoning Group in AWS (Austin, TX). I work on writing provably correct code that is also fast.
Previously, I was a research engineer CryptoLab, a pioneering company for developing homomorphic encryption frameworks. I also fulfilled my military service in an alternative form by working for this company.
I received Ph.D. from Software Foundations Lab, Seoul National University in August, 2021. When I was a graduate student, I worked on clarifying the semantics of the intermediate representation of the LLVM compiler infrastructure and implementing compiler optimization validators.
I actively sent patches to LLVM (commits/patches) to (1) make LLVM IR semantics abide by a formal definition, and (2) resolve performance issues of the generated machine code after my patches. I also participated in developing Alive2 (https://alive2.llvm.org/), an automatic optimization validator (pull requests).
E-mail: firstname.lastname@example.org, email@example.com (personal), firstname.lastname@example.org (old)