This online document contains a number of useful resources to operate the Atelier B formal tool to model, to verify by proof, and to generate C source code. It is organized in 6 parts:
  • ​Getting your hands dirty: practical/technical information linked to the use of Atelier B
  • ​B Training courses: slides to understand B, practice B, and prove in B
  • ​Using B: some chapters extracted from the "B Language User Manual"
  • ​B examples: a collection of software models, from specification to implementation, down to source code in many cases
  • ​Event-B examples: a collection of system-level models
  • ​Glossary: a list of frequent specific words and expressions, and their meaning
  • ​References: several useful links