Xinyu Feng: Mechanized verification of preemptive OS kernels (invited talk). CPP 2017: 2