Why Would You Trust B ?

Abstract. The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself – or its implementation – is not formally checked. We address this question for the B, a widely used formal method that allows for the derivation of correct programs from specifications. Through a deep embedding of the B logic in Coq, we check the B theory but also implement B tools. Both aspects are illustrated by the description of a proved prover for the B logic.

• Type: Conference
• Year: 2007
• Where: LPAR
• Authors: Éric Jaeger, Catherine Dubois
• Keywords: Actual Level, Artificial Intelligence, Formal Method, LPAR 2007, Methods Provides Confidence