Links

Introduction

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