Abstract
Keywords:
Software verification, Hoare Logic, Theorem Proving, Caveat, Caduceus, Why, Coq, Simplify.
Abstract:
This 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.