Kanghee Park ☕️

Kanghee Park

Research Engineer

Harmonic

Summary

About Me

I am a Research Engineer at Harmonic. I completed my PhD in Computer Science and Engineering at UC San Diego in September 2026, advised by Loris D’Antoni. My research focuses on making AI more reliable and effective for formal verification.

Outside of work, I enjoy playing acoustic guitar and training for marathons.

Interests

Program Synthesis Program Analysis Formal Verification Proof Search
Education

  1. PhD Computer Science and Engineering

    UC San Diego (Transferred from UW-Madison)
    Research on scaling formal reasoning through modularization and abstraction. Supervised by Loris D’Antoni.

  2. MS Computer Science

    University of Wisconsin-Madison
    Supervised by Loris D’Antoni. Transferred to UC San Diego after 3 years.

  3. BS Computer Science and Mathematics

    Pohang University of Science and Technology
    Engineering’s Valedictorian, Summa Cum Laude
Selected Publications
Kanghee Park
Equal contribution
, Xuanyu Peng
Equal contribution
, Loris D'Antoni (2025). LOUD: Synthesizing Strongest and Weakest Specifications. OOPSLA 2025.
Code PDF
Kanghee Park, Timothy Zhou, Loris D'Antoni (2025). Flexible and Efficient Grammar-Constrained Decoding. ICML 2025.
Code PDF
Kanghee Park
Equal contribution
, Jiayu Wang
Equal contribution
, Taylor Berg-Kirkpatrick, Nadia Polikarpova, Loris D'Antoni (2024). Grammar-Aligned Decoding. In NeurIPS 2024.
Code PDF
Kanghee Park, Keith J.C. Johnson, Loris D'Antoni, Thomas Reps (2023). Modular System Synthesis. FMCAD 2023.
PDF
Kanghee Park, Loris D'Antoni, Thomas Reps (2023). Synthesizing Specifications. OOPSLA 2023.
Code PDF
All publications