Certifying low-level programs with hardware interrupts and preemptive threads.

Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo

Browse the full PLDI paper archive.