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.