A Simulation Expert’s Guide to Formally Proving SW Status and Interrupts