Towards Formally Verified Optimizing Compilation in Flight Control Software

Ricardo Bedin FrançA, Denis Favre-Felix, Xavier Leroy, Marc Pantel & Jean Souyris
This work presents a preliminary evaluation of the use of the CompCert formally specified and verified optimizing compiler for the development of level A critical flight control software. First, the motivation for choosing CompCert is presented, as well as the requirements and constraints for safety-critical avionics software. The main point is to allow optimized code generation by relying on the formal proof of correctness instead of the current un-optimized generation required to produce assembly code...