2021


  • 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.

2020


  • 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.

2019



2018


  • Jun 2018. Our paper “Reconciling High-level Optimizations and Low-level Code in LLVM” has been accepted at OOPSLA’18. See here.
  • Feb 2018. Our paper “Crellvm: Verified Credible Compilation for LLVM” has been accepted at PLDI’18. See here.

2017


  • Jun 2017. Our paper “Repairing Sequential Consistency in C/C++11″ received a PLDI'17 Distinguished Paper Award.
  • Mar 2017. Juneyoung Lee received a graduate scholarship from KFAS (Korea Foundation of Advanced Studies).
  • Feb 2017. Our paper “Taming Undefined Behavior in LLVM” has been accepted at PLDI’17. See here.
  • Feb 2017. Our paper “Repairing Sequential Consistency in C/C++11″ has been accepted at PLDI’17. See here.

2016


  • Oct 2016. Our paper “A Promising Semantics for Relaxed-Memory Concurrency” has been accepted at POPL’17. See here.
  • Jun 2016. Our technique “Lightweight Verification of Separate Compilation” has been applied to CompCert 2.7. See here.

2015


  • Oct 2015. Our paper “Lightweight Verification of Separate Compilation” has been accepted at POPL’16. See here.
  • May 2015. Our paper “Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language” has been accepted at ICFP’15. See here.
  • Mar 2015. Jeehoon Kang received a graduate scholarship from KFAS (Korea Foundation of Advanced Studies).
  • Feb 2015. Our paper “A Formal C Memory Model Supporting Integer-Pointer Casts” has been accepted at PLDI’15. See here.

2014


  • Apr 2014. Our paper “R2: An Efficient MCMC Sampler for Probabilistic Programs” has been accepted at AAAI’14 for oral presentation. See here.
  • Mar 2014. Yoonseung Kim received a graduate scholarship from KFAS (Korea Foundation of Advanced Studies).
  • Feb 2014. Our paper “Slicing Probabilistic Programs” has been accepted at PLDI’14. See here.

2013


  • Sep 2013. Software Foundations Lab started!