2018


  • Jul 2018. We developed a simpler and faster operational concurrency model for ARMv8 and RISC-V. See here.
  • 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.