My interest lies in formal verfication low-level concurrent data structures and systems. I am especially interested in modular and automatic verification of them using separation logic such as Iris.
Currently, I am researching on improving the automation of Diaframe, an automation tool for Iris. I wish to improve its usability in aiding the proof of more complex data sturctures and systems, scaling up to thousands of lines of proof code.
I am also interested in designing specifications for weak memory data sturctures, especially for ones that does not have a clear sequential specification.
- Email: email@example.com
- GitHub: Lee-Janggun
- Bibliography: ORCID, DBLP, Google Scholar
- Place: Rm. 4441, Bldg. E3-1, KAIST (+82-42-350-7878)
(2024) M.S. in Computer Science. KAIST (expected).
(2022) B.S. in Mathematical Sciences & Computer Science. KAIST.
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]