Code optimizations using formally verified properties
Yao Shi, Bernard Blackham, Gernot Heiser · 2013
Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are then used to prove that the code adheres to its specification.