FORMAL SEMANTICS · WEBASSEMBLY · MODEL CHECKING
Ph.D. Student in Computer Science and Engineering at POSTECH.
My research focuses on formal semantics, software verification, and model checking. I am currently working on WebAssembly, with particular interest in translating declarative language specifications into executable formal models for execution, search, and verification.
More broadly, I am interested in programming-language semantics, rewriting logic, automated reasoning, and formal verification.
I am broadly interested in programming-language semantics, formal verification, automated reasoning, and executable models.
Executable semantics and formal specifications of programming languages.
State-space exploration and temporal verification of programs and systems.
Formal modeling and verification of WebAssembly semantics and programs.
Executable formalization and reasoning using rewriting-based semantics.
Research and software projects I am currently working on or have led.
WebAssembly SpecTec semantics → executable Maude specifications
Spec2Maude is an automated translation pipeline from WebAssembly SpecTec semantics to Maude rewriting logic. It aims to preserve the source semantics while producing executable formal specifications that support execution, search, and model checking.
Led the development of a multilingual web platform connecting domestic and international dog adoptions.
Ph.D. Student in Computer Science and Engineering
Formal Reasoning & Verification Lab (FOREVER)
Advisor: Prof. Kyungmin Bae
B.S. in Applied Physics · B.E. in Computer Science
Department of Applied Physics
Division of Computer Science
Formal Reasoning & Verification Lab (FOREVER), POSTECH
Quality Management & Technical Support Team, Silcroadsoft
Selected academic honors, scholarships, and awards.
Hanyang University, Korea
2025 ERICA Software-Up! 7th SW Startup Hackathon, Hanyang University, Korea
Hanyang University, Korea
Academic Excellence · Hanyang University, Korea