Through the collaborative R&D project AIDOaRT , CLEARSY is going to develop a module within the Atelier B Interactive prover that can learn interactive theorem proving from the developer and adapt it to unsolved proofs.
The project is in line with last decade R&D on connecting with third party provers/solvers. Direct applications to safety critical software applications are expected, in particular for SIL4 applications in the railways and to support formal software development with the CLEARSY Safety Platform.
At the crossroad of software engineering, MDE and artificial intelligence, AIDOaRT is a 3-year H2020-ECSEL project involving 36 organizations, focusing on AI-augmented automation supporting modelling, coding, testing, monitoring and continuous development in Cyber-Physical Systems (CPS).