SFlab: News

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.
Apr 2019. Juneyoung Lee received the second prize in the Student Research Competition at 2019 European LLVM developers' meeting. Congratulations!
Feb 2019. Jeehoon Kang will work as a tenure-track faulty at KAIST School of Computing from March 2019. Congratulations!
Feb 2019. Jeehoon Kang received a PhD degree. Congratulations! His PhD thesis is avaliable here.
Feb 2019. Juneyoung Lee will present a talk "Safely Optimizing Casts between Pointers and Integers" at 2019 European LLVM developers' meeting.
Feb 2019. Our paper “Promising-ARM/RISC-V: a simpler and faster operational concurrency model” has been accepted at PLDI’19. 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.

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.

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.

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.

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.