Effective verification for low-level software with competing interrupts by Liang, L, Melham, T, Kroening, DHF, Schrammel, P, Tautschnig, M