A Simulation Expert’s Guide to Formally Verifying Software Status and Interrupts