Welcome to Software Foundations Lab!

News

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

More (Past) News

People

• Professor
  • Chung-Kil Hur
• Graduate Students
  • Yoonseung Kim
  • Youngju Song
  • Juneyoung Lee
  • YongHyun Kim
  • Sung-Hwan Lee
  • Minki Cho
  • Dongjoo Kim

More (Former) People

Research

Our research focuses on theoretically interesting software problems that are also practically useful.
Please see below for the details of our recent projects.

• Formal Semantics of low-level languages
  • Reconciling High-level Optimizations and Low-level Code in LLVM
  • Taming Undefined Behavior in LLVM
  • A Formal C Memory Model Supporting Integer-Pointer Casts
• Relaxed Memory Concurrency
  • Promising ARM/RISC-V: a simpler and faster operational concurrency model for ARMv8 and RISC-V
  • Repairing Sequential Consistency in C/C++11
  • A Promising Semantics for Relaxed-Memory Concurrency
• Compiler Verification
  • CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
  • AliveInLean: A Verified LLVM Peephole Optimization Verifier
  • Crellvm: Verified Credible Compilation for LLVM
  • Lightweight Verification of Separate Compilation

More (Past) Research

Contact

Professor: Room 426 Bldg 302, TEL: 02-880-1844
Students: Room 312-2 Bldg 302, TEL: 02-880-1865
Department of Computer Science and Engineering
Seoul National University
1 Gwanak-ro, Gwanak-gu, Seoul 08826
Republic of Korea