I am interested in program verification with formal methods which verify systems with mathematics and logic. My ultimate goal is to automate program verification, which has the potential to reduce errors and improve the safety and reliability of systems.
I received MS and PhD in Informatics from Nagoya University (Yuen & Nakazawa Lab), where I was advised by Koji Nakazawa and Shoji Yuen. Prior to my doctoral studies, I earned BS degree in Information Systems from Hanyang University.
My doctoral research was evaluated by a thesis committee consisting of Koji Nakazawa, Shoji Yuen, Yuichi Kaji, and Makoto Tatsuta.
Theory of computation
Logic; Separation logic; Hoare logic;
Program verification; Automated reasoning; Concurrency.
Yeonseok Lee. Theoretical Studies of Program Verification Based on Separation Logic, Doctoral Thesis (Nagoya University), March 2026. [HDL Link]
Yeonseok Lee and Koji Nakazawa. Incorrectness separation logic with arrays and pointer arithmetic. Journal of Information Processing, 33:826--839, November 2025. [DOI]
Yeonseok Lee and Koji Nakazawa. Relative completeness of incorrectness separation logic. In The 22nd Asian Symposium on Programming Languages and Systems (APLAS 2024), Kyoto, Japan, volume 15194 of Lecture Notes in Computer Science (LNCS), 2024. [DOI] [Slides]
Yeonseok Lee and Koji Nakazawa. Decidable entailment checking for concurrent separation logic with fractional permissions. Computer Software, 40, 2023. (Revised version of the proceeding in the 39th JSSST Annual Conference.). [DOI]