Why Would You Trust B?
| dc.creator | Jaeger, Eric | |
| dc.creator | Dubois, Catherine | |
| dc.date | 2009-02-23 | |
| dc.date.accessioned | 2026-07-07T12:45:35Z | |
| dc.date.available | 2026-07-07T12:45:35Z | |
| dc.description | 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. | |
| dc.description | 15 pages | |
| dc.identifier | https://arxiv.org/abs/0902.3858 | |
| dc.identifier | http://arxiv.org/abs/0902.3858 | |
| dc.identifier | Logic for Programming, Artificial Intelligence, and Reasoning, Yerevan : Arménie (2007) | |
| dc.identifier | doi:10.1007/978-3-540-75560-9 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/221131 | |
| dc.subject | Logic in Computer Science | |
| dc.title | Why Would You Trust B? | |
| dc.type | text |