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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Jaeger, É., & Dubois, C. (2007). Why would you trust B? In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4790 LNAI, pp. 288–302). Springer Verlag. https://doi.org/10.1007/978-3-540-75560-9_22
Mendeley helps you to discover research relevant for your work.