Mechanized Result Verification: an Industrial Application

We present part of an industrial project where mechanized theorem proving is used for the validation of a translator which generates safety critical software. In this project, the mechanized proof is decomposed in two parts: one is done `on-line`, at each run of the translator, by a custom prover which checks automatically that the result of each translation meets some verification conditions; the other is done `off-line`, once for all, interactively with a general purpose prover; the off-line proof shows that the verification conditions checked by the on-line prover are sufficient to guarantee the correctness of each translation. The provably correct verification conditions can thus be seen as specifications for the on-line prover. This approach is called mechanized result verification