Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads Xinyu Feng Toyota Technological Institute at Chicago Joint work with Zhong Shao (Yale),Yuan Dong (Tsinghua Univ.)and Yu Guo (USTC)Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads Xinyu Feng Toyota Technological Institute at Chicago Joint work with Zhong Shao (Yale), Yuan Dong (Tsinghua Univ.) and Yu Guo (USTC)