Sep 2023. Our paper “Stuttering for Free” has been accepted at OOPSLA’23. See here.
Apr 2023.Chung-Kil Hur is charing the Program Committee of APLAS 2023, which will take place on 26-29 November 2023 in Taipei, Taiwan. Submit your papers by 15 June 2023, AoE!
Apr 2023. Our paper “Fair Operational Semantics” has been accepted at PLDI’23. See here.
Apr 2023. Our paper “Putting Weak Memory in Order via a Promising Intermediate Representation” has been accepted at PLDI’23. See here.
Oct 2022. Our paper “Conditional Contextual Refinement” has been accepted at POPL’23. See here.
Feb 2022. Our paper “Sequential Reasoning for Optimizing Compilers under Weak Memory Concurrency” has been accepted at PLDI’22. See here.
Jun 2021. Our paper “Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL” has been accepted at CONCUR’21. See here.
May 2021. Our paper “Alive2: Bounded Translation Validation for LLVM” received a PLDI'21 Distinguished Paper Award.
Apr 2021. Our paper “An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation” has been accepted at CAV’21. See here.
Feb 2021. Our paper “Modular Data-Race-Freedom Guarantees in the Promising Semantics” has been accepted at PLDI’21. See here.
Feb 2021. Our paper “Alive2: Bounded Translation Validation for LLVM” has been accepted at PLDI’21. See here.
Aug 2020.Juneyoung Lee will give a keynote speech at the 2020 LLVM Developers' Meeting. See here for details. This is the first time a phd student is giving a keynote speech at the meeting. Congratulations!
Feb 2020. Our paper “Promising 2.0: Global Optimizations in Relaxed Memory Concurrency” has been accepted at PLDI’20. See here.
Jan 2020. Our paper “Interaction Trees: Representing Recursive and Impure Programs in Coq” received a POPL'20 Distinguished Paper Award.
Dec 2019. Our paper “An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction” has been accepted at CPP’20. See here.
Nov 2019. The freeze instruction proposed by our paper “Taming Undefined Behavior in LLVM” has been officially adopted by LLVM. See here for more details.
Nov 2019. Our paper “CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification” has been accepted at POPL’20. See here.
Nov 2019. Our paper “Interaction Trees: Representing Recursive and Impure Programs in Coq” has been accepted at POPL’20. See here.
Apr 2019. Our paper “AliveInLean: A Verified LLVM Peephole Optimization Verifier” has been accepted at CAV’19 as a tool paper. See here.
Our research focuses on theoretically interesting software problems that are also practically useful.
Please see below for the details of our recent projects.