Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis. - Thomas Sewell; Felix Kam; Gernot Heiser (RTAS, 2016)

High-assurance timing analysis for a high-assurance real-time operating system. - Thomas Sewell; Felix Kam; Gernot Heiser (Real Time Syst., 2017)