Joonwon Choi.
I'm a graduate student at MIT CSAIL, currently co-advised by Adam Chlipala and Arvind. I'm interested in formal verification for any computer systems that are hard to believe to be correct. I'm an advocate of mechanized proofs, I like to prove something with Coq. I don't believe things not proven.
CV: [pdf]
Office: 32-G804, Stata Center, 32 Vassar St, Cambridge, MA 02139
Email: joonwonc@mit.edu | Phone: +1-339-225-5940
Research Interests
My current research interests are as follows:
- Formal synthesis of protocols in message-passing systems.
- Formal verification for correct hardware design and synthesis, based on modular proof. Take a look at the Kami project page for details
- Formal verification of realistic processors.
Education
- 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) - Feb 2006, graduated from Incheon Science High School
Publication
- Kami: A Platform for High-Level Parametric Hardware
Specification and its Modular Verification.
[pdf]
, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind.
Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP'17). September 2017.
- An Inlining Approach to Formal Hardware Semantics.
[pdf]
M.S. Thesis in Electrical Engineering and Computer Science, Massachusetts Institute of Technology.
- Crellvm: Verified Credible Compilation for LLVM
[draft
pdf]
Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, , Chung-Kil Hur, and Kwangkeun Yi.
To appear in Proceedings of the ACM SIGPLAN 2018 Conference on Programming Language Design and Implementation (PLDI'18). June 2018.
Awards and Honors
- Sep 2014 - Current, Kwanjeong Educational Fellowship
- Sep 2014 - Current, MIT Emerson Scholarship for Private Music Study
- Feb 2013, Top Honor (summa cum laude) Certification
- Mar 2006 - Feb 2013, Presidential Science Scholarship
Teaching Experience
- Spring 2017, Teaching Assistant, MIT 6.887: Formal Reasoning About Programs
- Fall 2013, Teaching Assistant, SNU 4190.310: Programming Languages
Work Experience
- Apr 2009 - Oct 2011, Software Engineer, allm Games (Skilled Industry Personnel)
- Jan 2009 - Apr 2009, Software Engineering Intern(SWE), Google Korea
- Jul 2007 - Aug 2007, Intern, SK Communications