Modular, compositional, and executable formal semantics for LLVM IR. - Yannick Zakowski; Calvin Beck; Irene Yoon 001; Ilia Zaichuk; Vadim Zaliva; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

A Two-Phase Infinite/Finite Low-Level Memory Model. - Calvin Beck; Irene Yoon 001; Hanxi Chen; Yannick Zakowski; Steve Zdancewic (CoRR, 2024)

A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. - Calvin Beck; Irene Yoon 001; Hanxi Chen; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2024)

Vellvm: Formalizing the Informal LLVM - (Experience Report). - Calvin Beck; Hanxi Chen; Steve Zdancewic (NFM, 2025)