Sunho Park (박선호)

I am a Master’s Student at KAIST School of Computing. I am interested in developing and reasoning about safe algorithms, and I have been doing formal verification of concurrent objects with Iris framework on Coq proof assistant. I have particular interest in verification under realistic and complex situations, e.g. weak memory models.

Contact

• Email: sunho.park@kaist.ac.kr
• GitHub: kingdoctor123
• Bibliography: ORCID, DBLP, Google Scholar
• Place: Rm. 4441, Bldg. E3-1, KAIST (+82-42-350-7878)

Education

• (2024 - Current) M.S. in Computer Science. KAIST.

• (2024) B.S. in Computer Science. KAIST.

Publications

• (PLDI 2025) Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic.
  Jaehwang Jung, Sunho Park, Janggun Lee, Jeho Yeon, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation (Distinguished Paper Award).
  [paper: doi, local] ​ ​ ​
  

• (PLDI 2025) Verifying Lock-Free Traversals in Relaxed Memory Separation Logic.
  Sunho Park, Jaehwang Jung, Janggun Lee, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ ​ ​
  

• (PLDI 2024) A Proof Recipe for Linearizability in Relaxed Memory Separation Logic.
  Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang .
  ACM SIGPLAN conference on Programming Languages Design and Implementation.
  [paper: doi, local] ​ [artifact: proofs] ​ ​
  

• (OOPSLA 2023) Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic.
  Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang .
  Object-oriented Programming, Systems, Languages, and Applications.
  [paper: doi, local] ​ [artifact: proofs] ​ ​