Joonwon Choi

Profile

I'm a formal-verification engineer at Apple, working on verifying memory subsystems. Before that, 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:

  • Kami: a framework to implement, specify, prove, and synthesize hardware components based on modularity.
  • Hemiola: a framework for structural design and proof of hierarchical cache-coherence protocols based on serializability.
  • Lightbulb: an end-to-end proof between hardware and software; I worked particularly on the correctness proof of a pipelined RISC-V processor designed in Kami.

email joonwonc at alum dot mit dot edu || phone +1-339-225-5940

article CV || workGitHub

Publication

  • Formal Semantics of Verilog, Revisited for Deductive Verification: A Coq-Embedded Verification Framework as a Use Case
    Joonwon Choi
    submitted.
  • Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols [paper] [presentation] [github]
    Joonwon Choi, 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]
    Joonwon Choi
    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, Joonwon Choi, 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]
    Joonwon Choi, 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, Joonwon Choi, 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, Joonwon Choi, 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]
    Joonwon Choi
    M.S. Thesis in Electrical Engineering and Computer Science, Massachusetts Institute of Technology.

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

Teaching Experience

Work Experience

  • Mar 2021 - Current, Formal Verification Engineer, 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, Software Engineering Intern(SWE), Google Korea