Verification-Enhanced Compiler Optimisation is a research activity in the Trusted Components part of the Trustworthy Systems project.
Aim: Reuse the existing formal specification to improve the compiler optimisations.
Overview: Formal program verification offers strong assurances 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.
We explore the overlap between formal verification and code optimization. We propose two approaches to reuse the invariants derived in formal proofs and integrate them into compilation. The first applies invariants extracted from the proof, while the second leverages the property of program safety (i.e., the absence of bugs). We reuse this information to improve the performance of generated object code.
Technical research challenges:
||Yao Shi, Bernard Blackham and Gernot Heiser|
Code optimizations using formally verified properties
Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 427–442, Indianapolis, USA, October, 2013