Interactively verifying a simple real-time scheduler

This paper describes the interactive verification of a simple interrupt-driven real-time scheduler written in the machine code language of the MIPS R3000 RISC processor. The formal verification was carried out using the interactive theorem prover Ergo.