Proving B with Atelier B

Overview & Synopsis

The article focuses on the continuous improvement of Atelier B’s automatic proof capabilities since its industrialisation in the 90s. The evolution of Atelier B addressed challenges in proof obligations generation and optimisation, adapting to new languages like Event-B and incorporating newer formats for easier analysis and third-party prover connections. Significant developments include enhancing the proof system to handle complex proof obligations efficiently and integrating external provers for improved proof capabilities. The article also showcases B’s industrial applications in critical sectors, emphasising the method’s importance in safety-critical software development and the ongoing efforts to facilitate proof activities and integrate AI for better proof automation.