B Method Training
– Level 3: Prove B

PROVE B

OBJECTIVES :

  • Learn to prove a B model with Atelier B.

AUDIENCE :

  • Any person who wishes to verify a B project.

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