Embedded in Academia

Looking for Missed Alarm Bugs in a Formal Verification Tool

Dataflow Analyses and Compiler Optimizations that Use Them, for Free

Why Do Peephole Optimizations Work?

Formal-Methods-Based Bugfinding for LLVM’s AArch64 Backend

High-Throughput, Formal-Methods-Assisted Fuzzing for LLVM

A Close Look at a Spinlock

llvm-reduce

Responsible and Effective Bugfinding

Alive2 Part 3: Things You Can and Can’t Do with Undef in LLVM

The Gods Pocket Peak Trail