- Learn to prove a B model with Atelier B.
- Any person who wishes to verify a B project.
1 – PRINCIPLES OF THE VERIFICATION ACTIVITY
The verification (“proof”) activity with Atelier B is divided into various phases:
- the use of an automatic prover to demonstrate most of the obligations of correct proof,
- an examination of remaining proof obligations to detect errors and
- the finalization of proof with an interactive prover.
2 – AUTOMATIC PROVER PRINCIPLES
- Description of the strategies and mechanisms of Atelier B automatic prover.
3 – USING THE AUTOMATIC PROVER
- Description of the principles for using the interactive prover,
- description of the controls of interactive proof,
- methodological recommendations for a proper interactive demonstration