Convincing Proofs for Program Certification

At the highest level of formal certification, the current research trend consists in providing evaluators with a formal checkable proof produced by automatic verification tools. The aim is to reduce the certification process to verifying the provided proof using a proof-checker. However, to date, no certified proof-checker has emerged. In addition, checkable proofs do not eliminate the need to validate the formalization of the verification problem. In this paper we consider the point of view of evaluators. We elaborate criteria that must be fulfilled by a formal proof in order to convince skeptical evaluators. Then, we present a methodology based on this notion of convincing proofs that requires simple formalizations to reach the level of confidence of formal certification. The key idea is to build a certified proof-checker – in collaboration with the evaluators – which is finally used to validate the proof provided by developers. We illustrate our approach on the correctness proof of a buffering protocol written in c that manages the data exchanges between concurrent tasks in avionics control systems.