Our Contributions A Hoare-style program logic for modular verification of low-level programs with interrupts and concurrency. Locks Condition Variables yield/sleep void acq_m(Lock *1); void wait_m(Lock *I,CV *cv); timer_handler void rel_m(Lock *I); void signal_m(CV *cv); void yield() cli/ void acq_h(Lock *1); void wait_h(Lock *I,CV *cv); void sleep() sti void rel_h(Lock *1); void signal_h(Lock *I,CV *cv); void acq_spin(Lock *I); void wait_bh(Lock *I,CV *cv); void rel_spin(Lock *I); void signal_bh(Lock *I,CV *cv); scheduler block unblock void scheduler() void blk(queue *q) int unblk(queue *q) node*deQueue(queue *q) void enQueue(queue q,node *n) ctxt switching codeOur Contributions A Hoare-style program logic for modular verification of low-level programs with interrupts and concurrency