Our research focuses on theoretically interesting software problems that are also practically useful.
Please see below for the details of our 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

• Putting Weak Memory in Order via a Promising Intermediate Representation
• Sequential Reasoning for Optimizing Compilers under Weak Memory Concurrency
• Modular Data-Race-Freedom Guarantees in the Promising Semantics
• Promising 2.0: Global Optimizations in 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

Probabilistic Programming

• R2: An Efficient MCMC Sampler for Probabilistic Programs
• Slicing Probabilistic Programs

Misc

• Shovel: A SAT-based Tool for Information Flow Alarm Classification