Verification-Enhanced Compiler Optimisation

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:

  • Extract information from the formal specification (semi-) automatically.
  • Integrate the formally verified properties into the compiler.
  • Keep program correctness with partially correct information and control the optimised code size.

Publications

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

People