Program Logic for Refinement and Multi-Level Interrupts Relational program logic for proving simulation relation Ownership-Transfer semantics for reasoning about multi-level interrupts Combining above two for our CSL-Style relational program logicProgram Logic for Refinement and Multi-Level Interrupts • Relational program logic for proving simulation relation • Ownership-Transfer semantics for reasoning about multi-level interrupts • Combining above two for our CSL-Style relational program logic