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
​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
​

Next - Getting Your Hands Dirty

Installation

Last modified 2mo ago

Copy link