Proof automation and support for interactive proof are key components in the application of formal methods for software and system design. For more than 20 years, CLEARSY has been maintaining and distributing special-purpose automatic and interactive theorem provers within Atelier B, an IDE for the B method, a formal framework for the development of safety-critical software components, and for Event-B, a formal notation for system design and analysis.
To complement these tools, CLEARSY has been actively pursuing R&D activities in the field of formal verification, reaching out to the academic community. In 2012-2016, CLEARSY was partner of the BWare project, funded by French national research agency ANR, where the application of the deductive program verification platform Why3 was explored. An important result of this project was “iapa”, a new component in Atelier B, that let the user apply off-the-shelf provers to proof obligations, using Why3 as gateway.
Starting 2017, in the ANR-funded project DISCONT, CLEARSY explored the application of SMT solvers, resulting once again in the integration of Atelier B of two new functionalities to improve proof support. Firstly, SMT solvers can be used in a lightweight interaction as so-called hammers in the interactive prover, letting the user try to discharge sub-goals via SMT solving. Second, SMT solvers can be applied directly to raw proof obligations thanks to an deep encoding of B logic suitable for SMT verification.
Starting in 2022, CLEARSY will start two new collaborative projects on proof support, also funded by ANR: BLaSST and ICSPA.
BLaSST aims to increase the success rate of proof automation by improving the SMT encoding and explore new encodings, such as SAT and pseudo Boolean, which are suitable for fast automatic verification and refutation.
ICSPA will provide the theoretical and practical harness to increase confidence in the proof tools, also creating opportunities to integrate new formal verification technologies in Atelier B.