DBLP | Google Scholar

Doctoral Thesis

• Scaling Up Relaxed Memory Verification with Separation Logics (September 2024, last updated on September 2026) | DOI (October 2024).
• Thesis proposal (July 2020).

2025

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

2022

• 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. In PLDI 2022.
• Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations. Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer. In POPL 2022, with Distinguished Paper Award.

2021

• GhostCell: Separating Permissions from Data in Rust. Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer. In ICFP 2021.

2020

• Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn, Jules Villard. In CAV 2020.
• RustBelt Meets Relaxed Memory. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer. In POPL 2020. (Slides | Talk)
• Stacked Borrows: An Aliasing Model for Rust. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer. In POPL 2020.

2017

• Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis. In ECOOP 2017, with Best Paper Award.

Technical Reports

• [2026] Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic, at RocqPL 2026.
• [2025] A Formal Specification of the NOVA Microhypervisor’s ABI, talk given at FOSDEM 2025.
• [2024] Verifying a Virtual Machine Monitor.
• [2024] Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation, at PriSC 2024.
• [2024] Modularizing CPU semantics for Virtualization, at PriSC 2024.
• [2020] Technical Appendix: RustBelt Meets Relaxed Memory.
• [2017] Technical Appendix: Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.

Pre-MPI Publications

• Learning and practicing object-oriented programming using a collaborative web-based IDE. Vu Nguyen, Hai H. Dang, Kha N. Do, Thu D. Tran. In Frontiers in Education Conference (FIE) 2014.
• EduCo: An Integrated Social Environment for Teaching and Learning Software Engineering Courses. Hai H. Dang, Vu Nguyen, Kha N. Do, Thu D. Tran. In iiWAS 2014.
• An interactive Web-based IDE towards teaching and learning in programming courses. Hai T. Tran, Hai H. Dang, Kha N. Do, Thu D. Tran, Vu Nguyen. In TALE 2013.