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: sunho0371@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 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: Coq 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: Coq proofs] ​ ​