Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (ECOOP, 2017)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (Dagstuhl Artifacts Ser., 2017)

Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. - Azalea Raad; Josh Berdine; Hoang-Hai Dang; Derek Dreyer; Peter W. O'Hearn; Jules Villard (CAV (2), 2020)

RustBelt meets relaxed memory. - Hoang-Hai Dang; Jacques-Henri Jourdan; Jan-Oliver Kaiser; Derek Dreyer (Proc. ACM Program. Lang., 2020)

Stacked borrows: an aliasing model for Rust. - Ralf Jung 002; Hoang-Hai Dang; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2020)

GhostCell: separating permissions from data in Rust. - Joshua Yanovski; Hoang-Hai Dang; Ralf Jung 002; Derek Dreyer (Proc. ACM Program. Lang., 2021)

Compass: strong and compositional library specifications in relaxed memory separation logic. - Hoang-Hai Dang; Jaehwang Jung; Jaemin Choi; Duc-Than Nguyen; William Mansky; Jeehoon Kang; Derek Dreyer (PLDI, 2022)

Simuliris: a separation logic framework for verifying concurrent program optimizations. - Lennard Gäher; Michael Sammler; Simon Spies; Ralf Jung 002; Hoang-Hai Dang; Robbert Krebbers; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Scaling up relaxed memory verification with separation logics. - Hoang-Hai Dang (2024)

Modular, Full-System Verification. - Gregory Malecha; Hoang-Hai Dang; Paolo G. Giarrusso; Simon Hudon; Jan-Oliver Kaiser; David Swasey (HotOS, 2025)