Two decades of industrial exploitation of the B formal method.

The release of Atelier B 4.7 materializes two decades of industrial exploitation of the B formal method, with the support of 24 collaborative R&D projects for various topics such as formal data validation, safe program execution, mathematical proof, automated model refinement or VHDL generation.

Here are some significant metrics:

• More than 1 century.man for its development until now
• Bug-free generated software for more than 20 years of operation
• Guaranteed emergency braking for more than 30% of the world’s automatic metros and for several tens of billions of cumulative passengers
• Formally proven security policies for microcircuits in tens of millions of smart cards worldwide
• Safe opening of platform screen doors for the transit of billions of passengers