Formal Verification of Hand-Coded Software Some Industrial Experiments and Lessons Learnt

International audienceThis paper gives an account of an ongoing attempt to prove the safety properties, of a hand-coded safety critical embedded software of industrial size. The method used is based on annotating the C source files with assertions that encode the safety-related functional properties to be satisfied by the software, and then generating proof obligations to be discharged by some theorem provers. We discuss what has been achieved and what difficulties were encountered, from which we derive requirements regarding the evolution of the verification tools involved in that experiment