공지사항

CSE will be holding a special seminar with outstanding researchers.
Even if you are busy, we hope you will attend and have a special time with outstanding researchers.

1. Date & Time : 2025. 1. 7.(Tue), 14:00
2. Venue : 104 building, E104
3. Speaker: Ph.D. Juneyoung Lee (Amazon AWS)
4. Research areas: PL + Compilers
5. Talk title: Practical Software Verification and Its Impact: From Compiler to Cryptography
6. Abstract: This talk will introduce the latest trends of software verification techniques with respect to the engineering efforts for developing compilers and cryptographic libraries. For the compiler effort side, I will talk about the latest interactions between the LLVM open-source compiler project and its translation validation tool. The talk will also introduce the efforts on the LLVM developers side for clearer formal semantics of LLVM intermediate representations. For verification of cryptographic libraries, I will talk about the s2n-bignum project of AWS which is a verified cryptographic library written in assembly. Its functional correctness is proven in HOL Light, an interactive theorem prover, and also designed to be constant-time. s2n-bignum is being actively used by the servers of AWS thanks to its proven-to-be-correct property as well as fast performance.