এই পাঠটি: Effective verification for low-level software with competing interrupts