Outline OS Correctness Verification framework Program logic for refinement and multi-level interrupts Verifying uC/OSOutline • OS Correctness • Verification Framework – Program logic for refinement and multi-level interrupts • Verifying μC/OS-II