It's Time for Trustworthy Systems
Gernot Heiser, Toby Murray, Gerwin Klein · IEEE Security & Privacy · 2012
The time for truly trustworthy systems, backed by machine checked formal proof and analysis, has arrived. Over the past few decades, advances in formal verification and analysis technologies mean that these tools can now scale sufficiently to cover the entire software trusted computing base of appropriately designed real world systems.