Sunho Park (박선호)
This website might be outdated. Please refer to my personal website for recent updates.
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: park-sunho
-
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
-
(EuroSys 2026)
CofferOS: Hardening OS-level Virtualization with Rust.
Minkyu Jung, Chanshin Kwak, Junho Ahn, Sunho Park, Changjun Lee, Jongyul Kim, Jeehoon Kang, Youngjin Kwon .
European Conference on Computer Systems.
-
(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]