B Method Training
– Level 3: Prove B

PROGRAM

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