|
 
|
[JD07a] Why Would You Trust B ?
Conférence Internationale avec comité de lecture : LPAR'07 Logic for Programming Artificial Intelligence and Reasoning, Yerevan (Armenia), January 2007, pp.288-302, Series LNCS 4790,
motcle:
Résumé:
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.
Commentaires:
note
BibTeX
| @inproceedings { | |||
| JD07a, | |||
| title | = | "{Why Would You Trust B ?}", | |
| author | = | " E. Jaeger and C. Dubois ", | |
| booktitle | = | "{LPAR'07 Logic for Programming Artificial Intelligence and Reasoning, Yerevan (Armenia)}", | |
| year | = | 2007, | |
| month | = | "January", | |
| series | = | "LNCS 4790", | |
| pages | = | "288-302", | |
| note | = | "{note}", | |
| } | |||
