Proof of Properties in Avionics
Jean Souyris, Denis Favre-Félix · 2008
This paper presents the industrial use of a program proof method based on CAVEAT (C program prover developed by the commissariat à l’énergie atomique) in the verification process of a safety critical avionics program.