Joonwon Choi
I'm an Applied Scientist at Amazon Web Services (AWS), working on verifying the Neuron Compiler. Before that, I worked as a Formal Verification Tech Lead at Apple, working on verifying memory subsystems and fabric interconnects in Apple silicon. I completed a PhD in computer science at MIT CSAIL co-advised by Adam Chlipala and Arvind. During my PhD, I worked on formal verification of hardware using the Coq interactive theorem prover.
joonwonc at alum dot mit dot edu || +1-339-225-5940
Education
- Feb 2021, Ph.D., Electrical Engineering and Computer Science, Massachusetts Institute of Technology
- Jun 2016, M.S., Electrical Engineering and Computer Science, Massachusetts Institute of Technology
- Feb 2013, B.S. summa cum laude, Department of Computer Science and
Engineering, Seoul
National University
(Double major in Mathematics)
Publication
- Revamping Verilog Semantics for Foundational Verification
submitted.
- Hemiola: A DSL and Verification Tools to Guide Design and
Proof of Hierarchical Cache-Coherence Protocols
[paper]
[presentation]
[github]
, Adam Chlipala, and Arvind.
Proceedings of the International Conference on Computer-Aided Verification (CAV'22). August 2022.
- Structural Design and Proof of Hierarchical Cache-Coherence
Protocols
[thesis]
Ph.D. Thesis in Electrical Engineering and Computer Science, Massachusetts Institute of Technology.
- Integration Verification Across Software and Hardware for a
Simple Embedded System
[paper]
Andres Erbsen, Samuel Gruetter, , Clark Wood, and Adam Chlipala.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21). June 2021.
- Kami: A Platform for High-Level Parametric Hardware
Specification and its Modular Verification
[paper]
[github]
, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP'17). September 2017.
- EverCrypt: A Fast, Verified, Cross-Platform Cryptographic
Provider
[paper]
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, , Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella-Beguelin.
IEEE Symposium on Security and Privacy (SP'20), May 2020.
- Crellvm: Verified Credible Compilation for LLVM
[paper]
Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, , Chung-Kil Hur, and Kwangkeun Yi.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'18). June 2018.
- An Inlining Approach to Formal Hardware Semantics
[thesis]
M.S. Thesis in Electrical Engineering and Computer Science, Massachusetts Institute of Technology.
Work Experience
- Apr 2025 - Current, Senior Applied Scientist, AWS
- Mar 2021 - Apr 2025, Formal Verification Tech Lead, Apple
- Jul 2018 - Sep 2018, Research Intern, Microsoft Research Cambridge
- Apr 2009 - Oct 2011, Software Engineer, allm Games (Skilled Industry Personnel)
- Jan 2009 - Apr 2009, SWE Intern, Google Korea
Teaching Experience
- Spring 2017, Teaching Assistant, MIT 6.887: Formal Reasoning About Programs
- Fall 2013, Teaching Assistant, SNU 4190.310: Programming Languages
Academic Services
- Program Committee: VSTTE 2024, PLDI 2024, CAV 2020 AE
Awards and Honors
- Sep 2014 - May 2019, Kwanjeong Educational Fellowship
- Sep 2014 - May 2018, MIT Emerson Scholarship for Private Music Study
- Feb 2013, Top Honor (summa cum laude) Certification
- Mar 2006 - Feb 2013, Presidential Science Scholarship